@Martin sorry to bother you again on things we already discussed, but I still have a doubt. The first question you linked says that $G\upharpoonright \alpha = \{G(\beta):\beta<\alpha\}$ or what Kunen calls $\text{ran}(G\upharpoonright\alpha)$, while in his definition, if we think about $f:A\to B$ as a subset of $A\times B$ and $C\subset A$ then $f\upharpoonright C=f\cap C\times B$

that is a set of ordered that is interpreted as a function $C\to B$

am I getting lost in details or is that an important difference?

Also I think a simple example would help me, if I were to take $F:\mathbf{V}\to\mathbf{V}$ to be the identity, what would be the unique $G:\mathbf{ON}\to\mathbf{V}$ such that the theorem holds? What if $F$ sends ordinals into their successors and acts as the identity on the rest of $\mathbf{V}$?

that is a set of ordered pairs*

oh, wait, a sequence as in the answer is again a function, so I think it coincides with the usage in Kunen's book