 In PA one can define an elementary injective pairing function on numbers, e.g., \((n,m)\coloneqq 2^n\times3^m\). With the help of this function an infinite sequence of sets of natural numbers can be coded as a single set of natural numbers. The \(n^{th}\) section of set of natural numbers U is defined by \(U_n\,\coloneqq \,\{m:\,(n,m)\in U\}\). Using this coding, we can formulate a form of the axiom of choice for formulae \({F}\) in \(\cC\) by 