[proofplan]
We use the standard set-theoretic recursion principle for finite initial segments of $\mathbb{N}$ to construct, for each $n$, the unique finite chain of length $n$ starting at $x_1$ and advancing by $F$. The desired function sends $n$ to the last entry of this finite chain. The recursive identity follows by extending the chain of length $n$ by one more application of $F$, and uniqueness follows from the principle of mathematical induction on the set of indices where another candidate agrees with the constructed function.
[/proofplan]
[step:Construct the value at $n$ from the unique finite $F$-chain of length $n$]
We use the following foundational fact about finite initial segments of $\mathbb{N}$: for every $n \in \mathbb{N}$, there is a unique function
\begin{align*}
a_n:\{1,\dots,n\} \to X
\end{align*}
such that
\begin{align*}
a_n(1)=x_1
\end{align*}
and, for every $k \in \{1,\dots,n-1\}$,
\begin{align*}
a_n(k+1)=F(a_n(k)).
\end{align*}
This is the finite-sequence form of natural-number recursion, obtained in the usual set-theoretic construction of finite sequences.
Define
\begin{align*}
f:\mathbb{N} &\to X
\end{align*}
\begin{align*}
n &\mapsto a_n(n).
\end{align*}
This is a well-defined function because each $a_n$ exists uniquely and satisfies $a_n(n)\in X$.
[guided]
The purpose of this step is to avoid defining an infinite sequence by recursion before the recursion theorem has been proved. Instead, we use only finite chains, whose construction is part of the ordinary set-theoretic theory of finite sequences.
For each $n \in \mathbb{N}$, consider the finite set $\{1,\dots,n\}$. The finite-sequence recursion principle gives a unique map
\begin{align*}
a_n:\{1,\dots,n\} \to X
\end{align*}
with initial value
\begin{align*}
a_n(1)=x_1
\end{align*}
and successor rule
\begin{align*}
a_n(k+1)=F(a_n(k))
\end{align*}
for every $k \in \{1,\dots,n-1\}$. The hypotheses needed here are exactly that $x_1 \in X$ and $F:X\to X$, because once $a_n(k)\in X$, the value $F(a_n(k))$ again belongs to $X$.
Now define the infinite candidate by taking the terminal value of each finite chain:
\begin{align*}
f:\mathbb{N} &\to X
\end{align*}
\begin{align*}
n &\mapsto a_n(n).
\end{align*}
The codomain is $X$ because $a_n$ is a map into $X$. The definition is single-valued because the finite chain $a_n$ is unique for each fixed $n$.
[/guided]
[/step]
[step:Verify the initial condition and recursive identity]
For $n=1$, the finite chain $a_1:\{1\}\to X$ satisfies $a_1(1)=x_1$, so
\begin{align*}
f(1)=a_1(1)=x_1.
\end{align*}
Let $n\in\mathbb{N}$. The restrictions $a_{n+1}|_{\{1,\dots,n\}}$ and $a_n$ are both functions $\{1,\dots,n\}\to X$ with initial value $x_1$ and the same successor rule on $\{1,\dots,n-1\}$. By uniqueness of the finite chain of length $n$,
\begin{align*}
a_{n+1}(k)=a_n(k)
\end{align*}
for every $k\in\{1,\dots,n\}$. In particular,
\begin{align*}
a_{n+1}(n)=a_n(n).
\end{align*}
Using the defining successor rule for $a_{n+1}$ at the index $n$, we obtain
\begin{align*}
f(n+1)=a_{n+1}(n+1)=F(a_{n+1}(n))=F(a_n(n))=F(f(n)).
\end{align*}
Thus $f$ satisfies both required conditions.
[/step]
[step:Prove uniqueness by induction on the agreement set]
Let
\begin{align*}
g:\mathbb{N}\to X
\end{align*}
be any function satisfying $g(1)=x_1$ and
\begin{align*}
g(n+1)=F(g(n))
\end{align*}
for every $n\in\mathbb{N}$. Define the agreement set
\begin{align*}
A:=\{n\in\mathbb{N}:g(n)=f(n)\}.
\end{align*}
Since $g(1)=x_1=f(1)$, we have $1\in A$.
Now let $n\in A$. Then $g(n)=f(n)$, and the recursive identities for $g$ and $f$ give
\begin{align*}
g(n+1)=F(g(n))=F(f(n))=f(n+1).
\end{align*}
Hence $n+1\in A$. By the principle of mathematical induction, $A=\mathbb{N}$. Therefore $g(n)=f(n)$ for every $n\in\mathbb{N}$, so $g=f$ as functions $\mathbb{N}\to X$.
Existence was established by the construction of $f$, and uniqueness has just been proved. This completes the proof.
[/step]
