Recursion Theorem:
Let $A$ be a set, $a\in A$, and $f \colon A\to A$ a mapping. Then there exists a unique mapping $g \colon \Bbb N\to A$ such that
1. $g(0)=a$
2. $g(n+1)=f(g(n))$
I formalize a proof based on the comments of Noah Schweber at here and here .
Fix $a\in A$. Let $Y=\{(n,x)\in\mathbb{N}\times A\mid \text{ there exist a sequence of length}$ $n$, in which first term is $a$, last term is $x$, and each term after the first is $f$ of the previous term$\}$.
Now we prove by induction: for each $n\in \mathbb{N}$, there exists a unique $y\in A$ such that $(n,y)\in\mathbb{N}\times A$.
For $n=0\implies$ only $y=a$ such that $(0,a)\in Y$. Assume that for $n=k$ there exists a unique $y\in A$ such that $(k,y)\in Y\implies$ for $n=k+1$, there exits a unique $f(y)$ such that $(k+1,f(y))\in Y$.
$\implies$ For all $n\in \mathbb{N}$, there exists a unique $y\in A$ such that $(n,y)\in Y$
$\implies$ Set $Y$ defines a function $g \colon \Bbb N\to A$ such that
1. $g(0)=a$
2. $g(n+1)=f(g(n))$
Please check my proof above! Many thanks!