If $a$ is an element of a well ordered set $W$, and if $X$ is an arbitrary set, then by a sequence of type $a$ in $X$ we shall mean a function from
the initial segment of $a\in W$ into $X$.
A sequence function of type $W$ in $X$ is a function $f$ whose domain consists
of all sequences of type $a$ in $X$, for all elements $a\in W$, and whose range is
included in $X$.
Transfinite recursion theorem. If $W$ is a well ordered set, and if $f$ is
a sequence function of type $W$ in a set $X$, then there exists a unique function $U:W\to X$ such that $U(a)=f(U^{a})$ for each $a\in W$.
Where $U^{a}=U\vert s(a)$.
PROOF. The proof of uniqueness is an easy transfinite induction. […] Call a subset $A$ of $W\times X$ $f$-closed if it has the following property: whenever $a\in W$ and $t$ is a sequence of type $a$ included in $A$ (that is, $(c,t(c)) \in A$ for all $c$ in the initial segment $s(a)$), then $(a,f(t))\in A$. Since $W\times X$ itself
is $f$-closed, such sets do exist; let $U$ be the intersection of them all. Since $U$ itself
is $f$-closed, it remains only to prove that U is a function. We are to prove, in other words, that for each $c\in W$ there exists at most one element $x\in X$ such that $(c,x)\in U$. (Explicitly: if both $(c,x)$ and $(c,y)$ belong to $C$, then $x=y$.) The proof is inductive. Let $S$ be the set of all those elements of $W$ for which it is indeed true that(c,x)\in U for at most one $x$. We shall prove that if $s(a)\in S$, then $a\in S$. To say that $s(a)\in S$ means that if $c<a$ in $W$, then there exists a unique element $x\in X$ such that $(c,x)\in U$. The correspondence $c\to x$ thereby defined is a sequence of type $a$, say $t$, and $t\subseteq U$. If $a$ does not belong to $S$, then $(a,y)\in U$ for some $y$ different from $f(t)$ Assertion: the set $U-\{(a,y)\}$
is $f$-closed. This means that if $b\in W$ and if $r$ is a sequence of type $b$ included in $U-\{(a,y)\}$, then $(b,f(r))\in U-\{(a,y)\}$. Indeed, if $\mathbf{b=a}$, then r must be t
(by the uniqueness assertion of the theorem), […]
How so? The uniqueness assertion is that only one such function $U$ abides the theorem, but we've yet to establish $U$ as a function at all, so it should have no bearing on this.
(Source: Halmos's Naive Set Theory, pp.70-71.)
Best Answer
Halmos could have been clearer there. He's not referring to the uniqueness assertion about $U$ specifically, but rather the uniqueness assertion of the theorem generally, which he's applying to a different function.
At the specific point in the proof you highlighted, $r$ and $t$ are both functions from the well-ordered set $s(a)$ into $X$, $f$ restricts to a sequence function of type $s(a)$ in $X$, and the conditions $$r(x)=f(r^x)\qquad\text{and}\qquad t(x)=f(t^x)$$ hold for all $x\in s(a)$ since $s(a)\subseteq S$; $r,t\subseteq U$; and $U$ is $f$-closed. So by the uniqueness assertion of the theorem applied to $r$ and $t$, it follows that $r=t$.