The role of Axiom Schema of Replacement in the proof of Transfinite Recursion Theorem 
Transfinite Recursion Theorem:
Let $G:V\to V$ be a class function. Then there is a unique function $F:\operatorname{Ord}\to V$ such that $$\forall \alpha\in \operatorname{Ord}:F(\alpha)=G(F\restriction\alpha)$$


I found that the proof of this theorem often follows:

*

*First, it proves that


For all $\alpha\in\operatorname{Ord}$, there exists a unique function $f_{\alpha}$ that satisfies
(1) $\operatorname{dom}f_{\alpha} = \alpha+1$
(2) $\forall \beta\le\alpha:f_{\alpha}(\beta) = G(f_{\alpha}\restriction\beta)$



*Second, it defines $F$

For all $\alpha\in\operatorname{Ord}$, $F(\alpha):=f_{\alpha}(\alpha)$.



*It proves that $F\restriction\alpha$ is a set with the following reasoning


We have $F\restriction\alpha=\{\langle \beta,F(\beta)\rangle\mid \beta<\alpha\}$, so by Axiom of Schema Replacement, $F\restriction\alpha$ is a set.


My questions:

*

*Of my understanding, After define $F$ by $\forall\alpha\in\operatorname{Ord}:F(\alpha):=f_{\alpha}(\alpha)$. I think I've finished our task, which is to define $F$.

I'm unable to understand why the proof goes on to prove that $F\restriction\alpha$ is a set for all $\alpha\in\operatorname{Ord}$.


*Of my understanding, $F$ is a function and $F\restriction\alpha$ is a restriction on $F$ and thus is a set.

I'm unable to understand what is the role of Axiom of Schema Replacement here.
Thank you so much for your response!
 A: How can you prove that $F\restriction\alpha$ is a set otherwise? This is literally a way to formulate the Replacement axiom schema: a class function restricted to a set is a set.
The point is that if you want to argue that $F(\alpha)=G(F\restriction\alpha)$, then you need to prove that $F\restriction\alpha$ is in the domain of $G$, or in other words, a set. Arguably, you could prove that $F\restriction\alpha+1=f_\alpha$, but this too will require you to appeal to Replacement (or its formulation via transfinite induction).
One good way to see this is to try and recreate the proof in a setting where we know it is bound to fail. Work in $V_{\omega+\omega}$ and consider $G(x)=\omega+n$  if $x\in V_{\omega+n+1}\setminus V_{\omega+n}$, or if $x\in V_{n+1}\setminus V_n$, and otherwise $G(x)=0$.
Now define by recursion this $F$. Then $F(0)=G(\varnothing)=0$, then $F(1)=G(F\restriction 1)=\omega+k$ for some appropriate $k$ (depending on your coding of ordered pairs and functions, of course). As you continue on, you realize that $F\restriction\omega$ is no longer a set. So how could you define $F(\omega)$? 
