In my textbook on computability theory there's a Lemma that's a special case of the Knaster-Tarski and Kleene fixpoint theorems. The lemma states:
Let $a \in \mathbb{N} ,\ g:\mathbb{N} \rightarrow \mathbb{N}$.
There exists exactly one function, $f: \mathbb{N} \rightarrow \mathbb{N}$ so that:
$
\left\{
\begin{array}{ll}
f(0) = a \\
f(Sx) = g(f(x)) \ (*) \\
\end{array}
\right.
$
Where S is the successor function.
Then a proof of the lemma follows which begins by showing that such an f exists and then that is unique.
The proof of existence is the following:
Using induction we consecutively construct the functions $f_0, f_1, ...$ where $dom(f_i) = \left \{0, 1, ..., i \right \}$ so that $f_i(0) = a$ and $f_i(n+1) = g(f_i(n)), \forall n < i$.
All of $f_i$ share the same values in their common domain ($f_0 \sqsubseteq f_1 \sqsubseteq f_2 \sqsubseteq \ ...$).
We now define: $f(n) = f_n(n),\ \forall n \in \mathbb{N}$. $f$ satisfies $(*)$ so we showed existence.
My question is, what do we mean by "proving existence" and why do we need this kind of proof to show that such a function exists? It seems evident to me that such a function would exist and my idea of a proof would be the following:
$f(0) = a$ therefore $f$ is well defined for $x = 0$ and $f(0) \in \mathbb{N}$.
Assuming $f(n)$ is well defined for $x = n$ and $f(n) \in \mathbb{N}$, then also $f(n+1)$ is well defined for $x = n+1$ and $f(n+1) \in \mathbb{N}$:
$f(n) \in \mathbb{N}$ so $g(f(n))$ is well defined and $\in \mathbb{N}$ so the same holds true for $f(n+1) = g(f(n))$.
By induction, $f$ exists and is well defined for all $n \in \mathbb{N}$.
Is my proof not sufficient?