Definition S.AN.1
Let N be a set.
We define that
(N,s,0) satisfies the axioms of natural numbers if and only if

A.S.AN.1   0:-N,
A.S.AN.2   s:N-1-1->N\{0},
A.S.AN.3   /\(A:-P(N)) [(0:-A and /\(n:-A) s(n):-A) => A = N].

Remark: We will often write (N,s,0) satisfies ANN.

Theorem S.AN.2
If (N,s,0) satisfies ANN then s:N-onto->N\{0}.

Let A = {n:-N\{0}|\/(k:-N) s(k)=n} u {0}.
We will show that A = N.
It is obvious that 0:-A.
Take any n:-A.
If n=0 then s(n)=s(0):-A.
Assume that n != 0.
Then there exists k:-N such that s(k)=n.
Since s(s(k)) = s(n), s(n):-A.
Thus by A.S.AN.3 A = N.
It shows that s:N-onto->N\{0}.

Theorem S.AN.3
If (N,s,0) satisfies ANN, Y is a set, 
y:-Y and g:NxY->Y
then there exists a unique function f:N->Y
such that f(0)=y and /\(n:-N) f(s(n)) = g(n,f(n)).

Let D(h) denote the domain of an arbitrary function h.

Let K = 
{ h:-P(NxY) | h is a function and 
  (0,y):-h and 
  /\(n:-N) s(n):-D(h) => n:-D(h) and h(s(n)) = g(n,h(n)) }.

Let f = u(K).
We will later show that f is a function.
Let A = {n:-N | \/(z:-Y) (n,z):-f}.
Notice that if f is a function then A is the domain of f.

We will show that A = N.

Since {(0,y)}:-K, 0:-A.
Take any n:-A.
There exists z:-Y such that (n,z):-f.
Hence there exists h:-K such that h(n) = z.
If s(n):-D(h) then s(n):-A.
Assume that !(s(n):-D(h)).
We construct function h1.
Let D(h1) = D(h) u {s(n)} and

         / h(k)  for k:-D(h),
h1(k) = { 
         \ g(n,z) for k = s(n).

It is easy to show that h1:-K.
Hence (s(n),g(n,z)):-h1 c f.
So s(n):-A.
Now by A.S.AN.3 A = N.

Let D = {n:-N | /\(y1,y2:-Y) (n,y1),(n,y2):-f => y1 = y2}.
We will show that D = N.

It is easy to show that 0:-D.
Take any n:-D.
There exists a unique z:-Y such that (n,z):-f.
Take any h:-K such that s(n):-D(h).
Then h(s(n)) = g(n,h(n)).
Since n:-D and (n,h(n)):-f, h(n) = z.
Hence h(s(n)) = g(n,z).
But h:-K was arbitralily chosen.
Hence /\(h:-K) h(s(n)) = g(n,z).
So s(n):-D.
Now by A.S.AN.3 D = N.

Since A = D = N, f:N->Y.

It is obvious that f(0) = y. 
We will show that /\(n:-N) f(s(n)) = g(n,f(n)).

Take any n:-N.
There exists h:-K such that h(s(n)) = g(n,h(n)).
Since h c f, f(s(n)) = g(n,s(n)).

Notice that f:-K.
Since f:-K, f is unique.

Theorem S.AN.4
If (N,s,0) and (N',s',0') satisfy ANN
then there exists a unique function f:N->N'
such that f(0)=0' and /\(n:-N) f(s(n)) = s'(f(n)).
Moreover f:N-1-1-onto->N'.

(N,s,0) satisfies ANN.
By Theorem S.AN.3 there exists an unique f:N->N'
such that f(0) = 0' and /\(n:-N) f(s(n)) = s'(f(n)).
We have to show that f:N-1-1-onto->N'.

We will show that f:N-onto->N'.
D = {n':-N'|\/(n:-N) f(n)=n'}
It is obvious that 0':-D.
Take any n':-D.
There exists n:-N such that f(n) = n'.
Then f(s(n)) = s'(f(n)) = s'(n').
Hence s'(n'):-D.
Since (N',s',0') satisfies ANN, D = N'.
Thus f:N-onto->N'

We will show that f:N-1-1->N'.
A = {n':-N | /\(n1,n2:-N) f(n1)=f(n2)=n' => n1=n2}
We will show that 0':-A.
Assume to the contrary that 
there exists n!=0 such that f(n)=0'.
By Theorem S.AN.2, there exists k:-N
such that s(k) = n.
Hence 0'=f(n)=f(s(k))=s'(f(k)). Contradiction with A.S.AN.2.
Thus 0':-A.
Take any n':-A.
Take any n1,n2:-N such that f(n1)=f(n2)=s'(n').
Since f(0)=0', n1!=0 and n2!=0.
Hence there exists k1,k2:-N such that s(k1)=n1, s(k2)=n2.
So f(s(k1))=f(s(k2))=s'(n'). 
Then s'(f(k1))=s'(f(k2))=s'(n').
Since s:N'-1-1->N', f(k1)=f(k2)=n'.
Since n':-A, k1=k2.
Hence n1 = n2.
Thus s(n'):-A.
By A.S.AN 3 A = N.
Thus f:N-1-1->N'.
This completes the proof.