Proof of Definition of Sequences by Recursion on the Natural Numbers

Let $Y=\mathbb{N}\times X$ and let $\ast:Y\times Y\to Y$ be the binary operation $(m,x)\ast y=\bigl(S(m),f(m,x)\bigr)$. For $n\in\mathbb{N}$, apply Existence and Uniqueness of Iterates of a Binary Operation on $Y$ with the constant map $[n]\to Y$ of value $(1,a)$: there is exactly one map $\tau_{n}:[n]\to Y$ with

for every $m\in\mathbb{N}$ with $S(m)\in[n]$.

Step 1 (consistency). Let $n\in\mathbb{N}$. By claim 3 of Basic Properties of Initial Segments of the Natural Numbers, $[n]\subseteq[S(n)]$. Let $\rho$ be the restriction of $\tau_{S(n)}$ to $[n]$. Then $\rho(1)=(1,a)$, and if $S(m)\in[n]$ then $m\in[n]$ (as noted in Existence and Uniqueness of Iterates of a Binary Operation) and $S(m)\in[S(n)]$, so $\rho(S(m))=\tau_{S(n)}(m)\ast(1,a)=\rho(m)\ast(1,a)$. By the uniqueness in Existence and Uniqueness of Iterates of a Binary Operation, $\rho=\tau_{n}$; that is, $\tau_{S(n)}(k)=\tau_{n}(k)$ for every $k\in[n]$.

Step 2 (the diagonal). Let $A$ be the set of $n\in\mathbb{N}$ such that the first coordinate of $\tau_{n}(n)$ is $n$. Then $1\in A$ since $\tau_{1}(1)=(1,a)$. Let $n\in A$ and write $\tau_{n}(n)=(n,x)$. Since $n\in[n]$ and $S(n)\in[S(n)]$ by claim 1 of Basic Properties of Initial Segments of the Natural Numbers, the recursion for $\tau_{S(n)}$ and Step 1 give

so $S(n)\in A$. By Principle of Induction for the Natural Numbers, $A=\mathbb{N}$.

Existence. For $n\in\mathbb{N}$ let $\sigma(n)\in X$ be the second coordinate of $\tau_{n}(n)$, so that $\tau_{n}(n)=(n,\sigma(n))$ by Step 2. Then $\sigma(1)=a$, and the display of Step 2 with $x=\sigma(n)$ gives $\tau_{S(n)}(S(n))=(S(n),f(n,\sigma(n)))$, that is, $\sigma(S(n))=f(n,\sigma(n))$ for every $n\in\mathbb{N}$. Thus $\sigma$ is a sequence in $X$ with the required properties.

Uniqueness. Let $\sigma':\mathbb{N}\to X$ also satisfy $\sigma'(1)=a$ and $\sigma'(S(n))=f(n,\sigma'(n))$ for every $n$, and let $B$ be the set of $n\in\mathbb{N}$ with $\sigma(n)=\sigma'(n)$. Then $1\in B$, and if $n\in B$ then $\sigma(S(n))=f(n,\sigma(n))=f(n,\sigma'(n))=\sigma'(S(n))$, so $S(n)\in B$. By Principle of Induction for the Natural Numbers, $B=\mathbb{N}$, so $\sigma'=\sigma$.