In a book I've found the following example of inductive definitions (let $n'=n\cup \{n\}$):
$\phi (0)=z,\ \phi(n')=f(\phi(n),n)$ [this will be definition (a)]
$\phi(0,a)=g(a), \ \phi(n',a)=H(\phi\vert(n'\times A),n,a)$ [this will be defintion (d)]
Of course (d) is more general than (a), so the existence of (d) implies the existance of (a). Let $g$ and $H$ be two functions belonging to $Z^A$ and $Z^{T\times \mathbb{N}\times A}$, respectively, and let $\phi$ be a function satisfying (d). Now let us define a sequence $\Psi: \Psi_n=\phi\vert(n'\times A)$, then:
$\Psi_0 =z^*=\{\langle \langle 0,a\rangle, g(a)\rangle :a\in A\}$
$\Psi_{n'}=\Psi_n\cup \{\langle \langle n', a\rangle, \phi(n',a)\rangle : a\in A \} =\Psi_n\cup \{\langle \langle n', a\rangle, H(\Psi_n,n,a)\rangle : a\in A \}=f(\Psi_n, n)$
Which means that $\Psi$ satisfies (a). Now the author writes "Now we shall prove the existence and uniqueness e of (a). This theorem shows that we are entitled to use definitions by induction of the type (a). According to the remark made above, this will imply the existence of functions satisfying formula (d)". I don't really get how proving that $\Psi$ satisfies (a) [assuming there exists a $\phi$ satisfying (a)] implies the existence of $\phi$ satisfying (d). Can anyone help me out? Thanks in advance.
