defpred S_{1}[ Nat] means for m, n being Nat st m + n = $1 holds

P_{1}[m,n];

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[n,m]

set k = m + n;

reconsider k = m + n as Element of NAT by ORDINAL1:def 12;

A8: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A8, A3);

then S_{1}[k]
;

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

P

A3: for k being Nat st S

S

proof

let m, n be Nat; :: thesis: P
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

for m, n being Nat st m + n = k + 1 holds

P_{1}[m,n]
_{1}[k + 1]
; :: thesis: verum

end;assume A4: S

for m, n being Nat st m + n = k + 1 holds

P

proof

hence
S
let m, n be Nat; :: thesis: ( m + n = k + 1 implies P_{1}[m,n] )

assume A5: m + n = k + 1 ; :: thesis: P_{1}[m,n]

end;assume A5: m + n = k + 1 ; :: thesis: P

per cases
( m = 0 or n = 0 or ( m <> 0 & n <> 0 ) )
;

end;

suppose A6:
( m <> 0 & n <> 0 )
; :: thesis: P_{1}[m,n]

then reconsider m9 = m - 1 as Element of NAT by NAT_1:20;

reconsider n9 = n - 1 as Element of NAT by A6, NAT_1:20;

m9 + n = k by A5;

then A7: P_{1}[m9,n9 + 1]
by A4;

m + n9 = k by A5;

then P_{1}[m9 + 1,n9]
by A4;

hence P_{1}[m,n]
by A2, A7; :: thesis: verum

end;reconsider n9 = n - 1 as Element of NAT by A6, NAT_1:20;

m9 + n = k by A5;

then A7: P

m + n9 = k by A5;

then P

hence P

set k = m + n;

reconsider k = m + n as Element of NAT by ORDINAL1:def 12;

A8: S

proof

for k being Nat holds S
let m, n be Nat; :: thesis: ( m + n = 0 implies P_{1}[m,n] )

assume m + n = 0 ; :: thesis: P_{1}[m,n]

then m = 0 ;

hence P_{1}[m,n]
by A1; :: thesis: verum

end;assume m + n = 0 ; :: thesis: P

then m = 0 ;

hence P

then S

hence P