formal definition of ordinal addition by recursion I'm reading Kunen's Set Theory, An Introduction to Independence Proofs (1980). On page 26 he explains how to introduce ordinal addition through recursion. For the sake of convenience i'll give the necessary information. What does Transfinite Recursion state? It states the following:

For any formula F$(x,y)$ we can define a formula G$(v,y)$ such that $$\forall x \; \exists ! \; y F(x,y) \to [\forall \alpha \; \exists ! \; y \; \mathrm{{\bf G}}(\alpha, y) \wedge \forall \alpha \exists x \exists y \; (\mathrm{{\bf G}}(\alpha, y) \wedge \mathrm{{\bf F}}(x, y) \wedge x = \mathrm{{\bf G}}|\alpha)],$$
  where $x = \mathrm{{\bf G}}|\alpha$ abbreviates
  $$ x \mathrm{\;is\; a \; function} \wedge \mathrm{dom}\;x = \alpha \wedge \forall \beta\in\mathrm{dom}\;x \;\; \mathrm{{\bf G}}(\beta,x(\beta))$$

So it says in fact that for any formula F$(x,y)$ which under certain conditions (if applied for instance by Comprehension Scheme to define a subset of some set) can define a set of ordered pairs (i.e. a relation) which is a function, then we can define a formula G$(v,y)$ which is also a function (it can be viewed as a function on the class of all ordinals) such that its value on any ordinal is exactly the value of F on the set which is the restriction of G to $\alpha$.
Next addition of ordinals by means of recursion is defined as follows. 

For any ordinal $\alpha$ a function $\mathrm{{\bf F}}_\alpha$ is defined so that $\mathrm{{\bf F}}_\alpha(x) = 0$ unless $x$ is a function with domain some ordinal $\beta$, in which case $\mathrm{{\bf F}}_\alpha(x)$ is $\alpha$ if $\beta = 0$, $S(x(\beta - 1))$ if $\beta$ is a successor and $\bigcup \{x(\xi) : \xi < \beta\}$ if $\beta$ is limit.

and here my troubles begin, in fact. First of all, The successor function $S$ was previously defined only for ordinals. Okay, we may count that $S(x) = x\cup \{x\}$ for any set $x$. But then the definition of $\mathrm{{\bf F}}_\alpha$ just doesn't make sense... i mean why it gives the desired result...
Then we get this unique function $\mathrm{{\bf G}}_\alpha$ (these formulas are treated as functions on classes) defined on ordinals such that $\forall \beta [\mathrm{{\bf G}}_\alpha(\beta) = \mathrm{{\bf F}}_\alpha(\mathrm{{\bf G}}_\alpha|\beta)]$. So this function gives us the addition in fact because, given any ordinal $\beta$, what is $\mathrm{{\bf G}}_\alpha |\beta$? it is, loosely speaking, the set of all ordered pairs $(a,y)$ such that $a\in\beta$ and $y = \mathrm{{\bf G}}_\alpha (\beta)$ (so it is a function which assigns to each ordinal $a \subset \beta$ some $y$ such that $y = \mathrm{{\bf G}}_\alpha(a)$)... And then we say that if $\beta$ is a successor, to calculate $\mathrm{{\bf G}}_\alpha (\beta)$ this $\mathrm{{\bf F}}_\alpha$ has to give out the successor of the value of $\mathrm{{\bf G}}_\alpha$ on $\beta - 1$ (i.e. it is $S(\alpha + \beta - 1)$ in fact, and if $\beta$ is limit, $\mathrm{{\bf F}}_\alpha$ has to give out an ordinal in fact which is the supremum of the values of $\mathrm{{\bf G}}_\alpha$ on ordinals lesser than $\beta$, i.e. it is (in different notation) $\bigcup \{\alpha + \xi | \xi < \beta\}$, so hence this function $\mathrm{{\bf G}}_\alpha$ defines the true addition (which can be defined without recursion as the unique ordinal isomorphic to a certain well-ordered set obtained on the basis of $\alpha$ and $\beta$)?
Okay, how can we define multiplication formally then? First we define this $\mathrm{{\bf F}}_\alpha$ to be again 0 unless $x$ is a function with domain some ordinal $\beta$. In case $x$ is as desired, define $\mathrm{{\bf F}}_\alpha(x)$ to be 0 if $\beta = 0$, $x(\beta - 1) + \alpha$ if $\beta$ is a successor and $\bigcup \{x(\xi)|\xi < \beta\}$ if $\beta$ is limit. And then we get the unique $\mathrm{{\bf G}}_\alpha$ which in fact for any ordinal $\beta$ gives us the $\alpha\cdot \beta$? is that right?
Thank you for reading and any suggestions...
 A: Your explanation of ordinal addition is correct.

this function $G_\alpha$ defines the true addition (which can be defined
  without recursion as the unique ordinal isomorphic to a certain
  well-ordered set obtained on the basis of $\alpha$ and $\beta$)?

Yes, $\alpha + \beta$ is the unique ordinal isomorphic to the well-order $(\{0\} \times \alpha \cup \{1\} \times \beta, \prec)$, where
$$
(x,y) \prec (x',y') \text{ iff } x < x' \vee (x=x' \wedge y < y')
$$
This can be visualized as follows

So we first list all elements of $\alpha$ with their usual order and then "add" $\beta$ with its usual order on top.
Your definition of ordinal multiplication is also correct. Maybe it helps to keep track what these different cases actually do. If $x$ is not as desired, let $F_\alpha(x) = 0$. For $x \colon \beta \rightarrow V$, where $\beta$ is an ordinal, do the following


*

*If $\beta = 0$, let $F_\alpha(x) = 0$ (this will give $\alpha \cdot 0$)

*If $\beta$ is a successor, let $F_\alpha(x) = x(\beta-1) + \alpha$ (and thus $\alpha \cdot \beta = \alpha \cdot (\beta-1) + \alpha$)

*If $\beta$ is a limit, let $F_\alpha(x) = \bigcup \{ x(\xi) \mid \xi < \beta \}$ (so finally $\alpha \cdot \beta = \sup_{\xi < \beta} \alpha \cdot \xi$)


Again, ordinal multiplication may be defined without recursion: $\alpha \cdot \beta$ is the unique ordinal isomorphic to the well-order $(\alpha \times \beta, \sqsubset)$, where
$$
(x,y) \sqsubset (x',y') \text{ iff } y < y' \vee (y=y' \wedge x < x')
$$
The corresponding picture is

