In T. Taos Analysis 1 book, on page 26, we have a proposition that tells us that recursive definitions are actually well-defined.
Proposition 2.1.16: Suppose for each naturla number $n$, wh have some function $f_n:\mathbb{N}\rightarrow\mathbb{N}$. Let $c$ be a natural number. Then we can assign a unique natural number $a_n$ to each natural number $n$, such that $a_0=c$ and $a_{n+1}=f_n(a_n)$ for each natural number $n$.
At this point only the axioms of the natural numbers are known. Now the author goes then on to develop set theory and explains how the natural numbers can be realized inside set theory and then says that now we can establish a rigorous version of the above proposition (as an exercise):
Exercise 3.5.12: This exercise will establish a rigorous version of Proposition 2.1.16. Let $f:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ be a function an $c$ a natural number. Show that there exists a function $a:\mathbb{N}\rightarrow\mathbb{N}$ such that $$a(0)=c$$and$$a(n+1)=f(n,a(n)).$$
Question: Supposing that we had already defined exactly what a function is an so on, then Proposition 2.1.16 seems to me to be a perfectly rigorous statement and its proof (via induction and the use of the Peano axioms) - which is much simpler than the proof of the exercise - a perfectly valid (i.e. not informal) proof. Is that true ?
(Does the other maybe say that Proposition 2.1.16 isn't rigorous and it's proof is only informal only because at that stage we don't have developed set theory ?)