Transfinite recursion

Let $h$ and $k$ be attempts and put $D = \mathrm{dom}(h) \cap \mathrm{dom}(k)$; then $D$ is an initial segment of $W$, being an intersection of two downward closed sets.

Put $S = \{a \in W : a \notin D \text{ or } h(a) = k(a)\}$ and suppose $W_{<a} \subseteq S$ for some $a \in D$; since $D$ is downward closed, $W_{<a} \subseteq D$, so $h$ and $k$ agree at every $x < a$, that is $h \restriction W_{<a} = k \restriction W_{<a}$, and therefore $h(a) = G(h \restriction W_{<a}) = G(k \restriction W_{<a}) = k(a)$, giving $a \in S$.

If instead $a \notin D$ then $a \in S$ outright, so for every $a \in W$ the implication "$W_{<a} \subseteq S$ implies $a \in S$" holds, and transfinite induction gives $S = W$: any two attempts agree on the intersection of their domains.

In particular, for each $a \in W$ there is at most one attempt with domain $W_{<a}$, and at most one attempt with domain $W$, since two of them would have that same set as the intersection of their domains.

Let $T = \{a \in W : \text{there is an attempt with domain } W_{<a}\}$, which is a set by Separation applied to $W$, and note that the attempt in question is unique when it exists.

Suppose $W_{<a} \subseteq T$; for each $b < a$ let $h_b$ be the unique attempt with domain $W_{<b}$ and put $h_b^{+} = h_b \cup \{(b, G(h_b))\}$, a function with domain $W_{\le b}$ which is again an attempt, because it agrees with $h_b$ below $b$ and $h_b^{+}(b) = G(h_b) = G(h_b^{+} \restriction W_{<b})$.

The assignment $b \mapsto h_b^{+}$ is given by a formula, so Replacement makes $\{h_b^{+} : b < a\}$ a set; let $u$ be the union of that set.

$u$ is a function: any two of the $h_b^{+}$ are attempts and therefore agree on the intersection of their domains, so no argument receives two different values.

$\mathrm{dom}(u)$ is the union of the sets $W_{\le b}$ for $b < a$, which equals $W_{<a}$: each such $W_{\le b}$ is contained in $W_{<a}$ by transitivity of the order, and each $x < a$ lies in $W_{\le x}$.

$u$ is an attempt with domain $W_{<a}$: for $c < a$ we have $u \restriction W_{<c} = h_c^{+} \restriction W_{<c} = h_c$ and $u(c) = h_c^{+}(c) = G(h_c)$, so $u(c) = G(u \restriction W_{<c})$.

Hence $a \in T$ whenever $W_{<a} \subseteq T$, so $T = W$ by transfinite induction: for every $a \in W$ there is a unique attempt $h_a$ with domain $W_{<a}$.

Replacement applied to the formula $a \mapsto h_a^{+} = h_a \cup \{(a, G(h_a))\}$ makes $\{h_a^{+} : a \in W\}$ a set; let $F$ be its union, which by the arguments of steps 8.1 and 8.2 is a function whose domain is the union of the sets $W_{\le a}$ for $a \in W$, namely $W$ itself.

$F$ satisfies the recursion: for $a \in W$ we get $F \restriction W_{<a} = h_a$ and $F(a) = h_a^{+}(a) = G(h_a)$, so $F(a) = G(F \restriction W_{<a})$, and in particular $F$ is an attempt with domain $W$.

Uniqueness: any function $F'$ with domain $W$ satisfying $F'(a) = G(F' \restriction W_{<a})$ for all $a$ is by definition an attempt with domain $W$, hence equals $F$.

There is therefore exactly one function $F$ with domain $W$ and $F(a) = G(F \restriction W_{<a})$ for every $a \in W$.