Question on the use of a parametric version of Transfinite Recursion Theorem in Introduction to Set Theory 3rd ed. by Hrbacek and Jech My question concerns a proof given on page 118 in the text Introduction to Set Theory 3rd ed. by Hrbacek and Jech.
The authors on page 117 prove a version of the transfinite recursion theorem (Theorem 4.11) that says given unary operations $G_1, G_2$, and $G_3$ there is an operation $F$ such that 
\begin{align*}
 &F(0)=G_1(0),\\
 &F(\alpha+1)=G_2(F(\alpha))\quad\text{for all ordinals $\alpha$, and}\\
 &F(\alpha)=G_3(F_\restriction \alpha)\quad\text{for all limit ordinals $\alpha$}.\\
\end{align*}
They then leave it up to the reader to devise a parametric version of Theorem 4.11.
I have determined this to be as follows: Given binary operations $G_1, G_2$, and $G_3$ there is an operation $F$ such that for all z
\begin{align*}
 &F(z,0)=G_1(z,0),\\
 &F(z,\alpha+1)=G_2(z,F_z(\alpha))\quad\text{for all ordinals $\alpha$, and}\\
 &F(z,\alpha)=G_3(z,F_z\restriction \alpha)\quad\text{for all limit ordinals $\alpha$}.\\
\end{align*}
Next they make use of the parametric version of Theorem 4.11 in the proof of Theorem 3.6 on page 118. 
Theorem 3.6 states:
\begin{align*}
&\text{Let G be an operation.}\\
&\text{For any set $a$ there is a unique infinite sequence $\langle a_n|n\in N \rangle$ such that} \\
&(a) a_0=a\\
&(b) a_{n+1}=G(a_n,n)\quad\text{for all $n\in N$}\\
\end{align*}
The proof for Theorem 3.6 given in the text is as follows:
\begin{align*}
&\text{Let G be an operation. We want to find, for every set $a$, a sequence}\\
&\text{$\langle a_n|n\in N \rangle$ such that $a_0=a$ and $a_{n+1}=G(a_n,n)$ for all $n\in N.$}\\
&\text{By the parametric version of the Transfinite Recursion Theorem 4.11,}\\
&\text{there is an operation $F$ such that $F(0)=a$ and $F(n+1)=G(F(n),n)$ for all $n\in N.$}\\
&\text{Now we apply the Axiom of Replacement: There exists a sequence $\langle a_n|n\in N \rangle$}\\
&\text{that is equal to $F\restriction \omega$ amd the Theorem follows.}\\
\end{align*}
Now, I understand everything in the proof of Theorem 3.6 except how the parametric version of Theorem 4.11 is used to derive the operation $F$ in the proof. Can can someone please help me fill in blanks?
 A: I have a feeling that the Theorem to be proved should be stated a bit more precisely as

Given any operation $G$ and any $a$ there is a unique infinite sequence $\langle a_n : n \in \omega \rangle$ such that 
  
  
*
  
*$a_0 = a$; and
  
*$a_{n+1} = G ( a_n )$.
  

I do not think that the parametrized version of transfinite recursion is needed (and the authors do not appear to actually use it).  Indeed, given $G$ and $a$ define the following three operations:


*

*$G_1 ( x ) = a$;

*$G_2 ( x ) = G ( x )$; and

*$G_3 ( x ) = a$.


(Note that as the result does not depend on the value of our operation at an infinite ordinal, the operation $G_3$ may be chosen arbitrarily.)  Then by the theorem on transfinite recursion there is a unique operation $F$ such that


*

*$F(0) = G_1(0) = a$;

*$F(\alpha+1) = G_2 ( F ( \alpha) ) = G ( F ( \alpha) )$; and

*$F(\alpha) = G_3 ( F \restriction \alpha ) = a$ for limit ordinals $\alpha > 0$.


Then the sequence $F \restriction \omega = \langle F(n) : n \in \omega \rangle$ will be as required.
