Theorem. Given a function $f: \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{N}$ and a constant $c \in \mathbb{N}$. Then there is a unique function $a:\mathbb{N} \rightarrow \mathbb{N}$ s.t. $a(0) = c \wedge (\forall n \in \mathbb{N}) \: a(n++) = f(n, a(n)) $.
Proof. We prove by induction that the theorem
$$ (\exists! a:\{ n \in \mathbb{N}: n \le N \} \rightarrow \mathbb{N}) \: \underbrace{a(0) = c}_{(i)} \wedge \underbrace{(\forall n \in \mathbb{N} : n < N) \: a(n++) = f(n, a(n))}_{(ii)}.$$
holds for each $N \in \mathbb{N}$.
"$N = 0$": $a(0) = c$ is a function from $\{0\}$ to $\mathbb{N}$ and satisfies property (i). Property (ii) holds vacuously since there are no natural numbers which are smaller than 0. The function $a$ is unique since if there was another function $a' \neq a$ such that $a'(0) = a(0) = c$, $a$ and $a'$ would, by definition of equality of functions, be equal. A contradiction.
"$N \rightarrow N++$": Assume the theorem holds for $N$ and define a new object $a'$ s.t.
$$ a'(n) =
\begin{cases}
a(n) & \text{if } n \le N \\
f(N, a(N)) & \text{if } n = N++.
\end{cases}
$$
It turns out that $a'$ is a function from $\{ n \in \mathbb{N} : n \le N++ \}$ to $\mathbb{N}$, since for each $n$ in the domain there's exactly one $a(n) \in \mathbb{N}$: By the induction hypothesis this is given for $n=0$ up to $N$. For $f$ being a function, it also holds for $n = N++$. Uniqueness: the induction hypothesis requires that $a(n):\{n \in \mathbb{N} : n \le N \} \rightarrow \mathbb{N}$ is unique whereas if there are two function $f, f': \{ (N, a(N)) \} \rightarrow \mathbb{N}$ such that $f(N, a(N)) = f'(N, a(N)) = a'(N++)$ they are equal. Finally, the induction hypothesis implies (i) and (ii) for $n < N$, where $a'(N++) = f(N, a(N))$ satisfies (ii) if $n < N++$.
$\Box$
2015 FEB 19 (v1.0)