Transfinite recursion

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

Put $S=\{a\in W:a\mathrm{\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\upharpoonright W_{<a}=k\upharpoonright W_{<a}$, and therefore $h(a)=G(h\upharpoonright W_{<a})=G(k\upharpoonright W_{<a})=k(a)$, giving $a\in S$.

If instead $a\mathrm{\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^{+}\upharpoonright 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{d}\mathrm{o}\mathrm{m}(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\upharpoonright W_{<c}=h_c^{+}\upharpoonright W_{<c}=h_c$ and $u(c)=h_c^{+}(c)=G(h_c)$, so $u(c)=G(u\upharpoonright 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\upharpoonright W_{<a}=h_a$ and $F(a)=h_a^{+}(a)=G(h_a)$, so $F(a)=G(F\upharpoonright W_{<a})$, and in particular $F$ is an attempt with domain $W$.

Uniqueness: any function $F^{\mathrm{\prime }}$ with domain $W$ satisfying $F^{\mathrm{\prime }}(a)=G(F^{\mathrm{\prime }}\upharpoonright 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\upharpoonright W_{<a})$ for every $a\in W$.