Successioni definite induttivamente

[ricky_e^x]

Utilizzerò a volte s(n) per indicare succ(n), il successivo di n
Devo dimostrare, utilizzando gli assiomi di peano e gli assiomi di base sulla teoria degli insiemi, la seguente proposizione:
Sia f: $\mathbb{N}$ $\times$ $\mathbb{N}$ $\rightarrow$ $\mathbb{N}$ una funzione, e sia c un numero naturale. Allora esiste una funzione $\sigma$ : $\mathbb{N}$ $\rightarrow$ $\mathbb{N}$ tale che $\sigma$(0) = c e $\sigma$(succ(n)) = f(n, $\sigma$(n))

Si dovrebbe dimostrare anche l'unicità, ma per adesso mi interessa capire se ho dimostrato bene l'esistenza, non sono sicuro della mia dimostrazione.

Ecco il mio tentativo: Prima di tutto ho dimostrato, è facile farlo, questi due lemmi (se si dice cosi lemma al plurale) che erano l'hint dell'esercizio.

Lemma 1:
Per ogni N $\in$ $\mathbb{N}$, esistono e sono unici, insiemi $A_{N}$ e $B_{N}$ tali che
i) $A_{N} \cup B_{N}$ = $\mathbb{N}$
ii) $A_{N} \cap B_{N}$ = $\emptyset$
iii) 0 $\in$ $A_{N}$
iv) succ(n) $\in$ $B_{N}$ non appena n $\in$ $B_{N}$
v) succ(N) $\in$ $B_{N}$
vi) n $\in$ $A_{N}$ e n $\ne$ N allora succ(n) $\in$ $A_{N}$

Lemma 2:
Utilizzando le notazioni precendeti, per ogni N $\in$ $\mathbb{N}$ esiste una unica funzione $\sigma_{N}$ : $A_{N}$ $\rightarrow$ $\mathbb{N}$ tale che $\sigma_{N}$(0) = c e $\sigma_{N}$(succ(n)) = f(n,$\sigma_{N}$(n)), per ogni n < N.

Adesso quindi posso utilizzare questi due lemmi e porre $\sigma(n)$ = $sigma_{n}(n)$ per ogni numero naturale n $\in$ $\mathbb{N}$ e da qui $\sigma(0)=c$, e $\sigma(s(n))$ = $\sigma_{s(n)}(s(n))$ = f(n, $\sigma_{s(n)}(n)$) e adesso noto che $\sigma_{s(n)}(n)$ = $\sigma_{n}(n)$, questo per il Lemma 2, perchè prendendo la restrizione di $\sigma_{s(n)}$ : $A_{n}$ $\rightarrow$ $N$, tale funzione sarà unica, e perciò uguale a $\sigma_{n}$ per tutti i naturali <= n. Da li' segue la tesi.