let k be non zero Element of NAT ; :: thesis: P_{1}[k]

defpred S_{1}[ Nat] means ex m being non zero Element of NAT st

( m = $1 & P_{1}[m] );

S_{1}[k]
from NAT_1:sch 9(A2);

k >= 1 by Lm1;

then ex m being non zero Element of NAT st

( m = k & P_{1}[m] )
by A6;

hence P_{1}[k]
; :: thesis: verum

defpred S

( m = $1 & P

A2: now :: thesis: for k being Nat st k >= 1 & ( for n being Nat st n >= 1 & n < k holds

S_{1}[n] ) holds

S_{1}[k]

A6:
for k being Nat st k >= 1 holds S

S

let k be Nat; :: thesis: ( k >= 1 & ( for n being Nat st n >= 1 & n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume that

A3: k >= 1 and

A4: for n being Nat st n >= 1 & n < k holds

S_{1}[n]
; :: thesis: S_{1}[k]

reconsider m = k as non zero Element of NAT by A3, ORDINAL1:def 12;

_{1}[m]
by A1;

hence S_{1}[k]
; :: thesis: verum

end;S

assume that

A3: k >= 1 and

A4: for n being Nat st n >= 1 & n < k holds

S

reconsider m = k as non zero Element of NAT by A3, ORDINAL1:def 12;

now :: thesis: for n being non zero Element of NAT st n < m holds

P_{1}[n]

then
PP

let n be non zero Element of NAT ; :: thesis: ( n < m implies P_{1}[n] )

assume A5: n < m ; :: thesis: P_{1}[n]

n >= 1 by Lm1;

then S_{1}[n]
by A4, A5;

hence P_{1}[n]
; :: thesis: verum

end;assume A5: n < m ; :: thesis: P

n >= 1 by Lm1;

then S

hence P

hence S

S

k >= 1 by Lm1;

then ex m being non zero Element of NAT st

( m = k & P

hence P