Can't find the demonstration of a theorem about recursion [closed]

$\def\nn{\mathbb{N}}$Consider the following procedure $f$ that requires an input from $\nn$:

  $f$ on input $n$ does the following:

    If $n = 0$:

      Output $a$.

    Otherwise:

      Output $g(f(n-1))$.

Note that $f(0) = a$. Also note that, given any $n \in \nn$, if $f(n)$ produces an output then $f(n+1)$ also does and furthermore $f(n+1) = g(f(n))$. Therefore by induction $f(n)$ produces an output for every $n \in \nn$, and $f(n+1) = g(f(n))$ for every $n \in \nn$. Thus $f$ is a function on $\nn$ satisfying the desired properties. Finally, it is easy to prove (by induction again) that any two functions satisfying the desired properties are the same.

The above proof is based on intuitive concepts, but these are not available in some formal systems such as ZF set theory. In ZF a function is defined as a set of ordered pairs (intended to encode (input,output) pairs) such that no two have the same first entry (each input maps to only one output). To build the desired $f$ we must build approximations.

The first step is to let $P(k)$ be the assertion that there is a function $h$ with domain $\{0..k\}$ such that $h(0) = a$ and $h(n+1) = g(h(n))$ for every $n \in \nn_{<k}$. Then clearly $P(0)$ and $P(k) \to P(k+1)$ for any $k \in \nn$, by explicit construction. Therefore by induction $P(k)$ for every $k \in \nn$.

The second step is to show that any function witnessing $P(k)$ is unique for the given $k \in \nn$. Again this is by induction.

The third step is to let $(h_k)_{k\in\nn}$ be a sequence of functions such that $h_k$ witnesses $P(k)$ for every $k \in \nn$, and show that $h_i$ and $h_j$ agree on $\{0..i\}$ for every $i,j \in \nn$ such that $i < j$. Again, this is by induction ('on $j$').

The fourth step is to let $f = \bigcup_{k\in\nn} h_k$, and to check that it is a function (which follows from the pairwise agreement) and that it satisfies the desired properties (which follows from the fact that $h_k$ witnesses $P(k)$ for every $k \in \nn$.

Longwinded? I agree. But that is just how it is. Essentially no shortcut.