@AlessandroCodenotti Yes, arjafi wrote in his answer $x_\alpha = G ( \langle x_\xi : \xi < \alpha \rangle )$, I would interpret $\langle x_\xi \rangle$ as a function.
The answer even explicitly mentions $F \upharpoonright \alpha = \langle x_\xi : \xi < \alpha \rangle$ in: "Note that since $\alpha$ is a set it follows that the restriction $F \upharpoonright \alpha = \langle x_\xi : \xi < \alpha \rangle$ is also set, and is thus a legitimate argument for the function $F$."
Quoting from Kunen, theorem 9.3, chapter 1 (in my edition): if $F:\mathbf{V}\to\mathbf{V}$, then there is a unique $G:\mathbf{ON}\to\mathbf{V}$ such that $\forall\alpha[G(\alpha)=F(G\upharpoonright\alpha)]$.
@AlessandroCodenotti I am afraid you do not get simple examples in this way, since $F$ gets a function as the input. (To be honest, I am a bit confused about what you get from the suggested $F$.)
I would try $F=\operatorname{ran}$ as a simple example. ($F$ assigns to any function - set of ordered pairs - its range. And it does not matter what are the values of $F$ for input which is not a function; since we never obtain such inputs as $G\upharpoonright\alpha$.)
I think you should get the identity $G(\alpha)=\alpha$ in this way.
Since $\alpha = \{\beta\in\mathbf{ON}; \beta<\alpha\} = \operatorname{ran} (id\upharpoonright\alpha)$.
I would agree that how the theorem on transfinite recursion is formalized might look a bit different from how it is used in real life. (I think you hardly ever explicitly writes down the function $F$ in a proof by transfinite induction. You simply write in such proof what $G(\alpha)$ is, if you know the previous values.)
@MartinSleziak I mistook this as an application of replacement saying that the image of $\alpha$ through $G$ is a set, but noticed my error later, it makes sense now
Your example was very helpful, thanks for your help!
