 CC2 : If \(P \subseteq \bN^{\bN} \times \bN\), and for each \(\ba \in \bN^{\bN}\) there exists \(n \in \bN\) such that \((\ba,n) \in P\), then there is a function \(f : \bN^{\bN} \rightarrow \bN\) such that \((\ba,f(\ba)) \in P\) for all \(\ba \in \bN^{\bN}\).