defpred S1[ Nat] means for m, n being Nat st m + n = $1 holds
P1[m,n];
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
for m, n being Nat st m + n = k + 1 holds
P1[m,n]
proof
let m, n be Nat; :: thesis: ( m + n = k + 1 implies P1[m,n] )
assume A5: m + n = k + 1 ; :: thesis: P1[m,n]
per cases ( m = 0 or n = 0 or ( m <> 0 & n <> 0 ) ) ;
suppose A6: ( m <> 0 & n <> 0 ) ; :: thesis: P1[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: P1[m9,n9 + 1] by A4;
m + n9 = k by A5;
then P1[m9 + 1,n9] by A4;
hence P1[m,n] by A2, A7; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
let m, n be Nat; :: thesis: P1[n,m]
set k = m + n;
reconsider k = m + n as Element of NAT by ORDINAL1:def 12;
A8: S1[ 0 ]
proof
let m, n be Nat; :: thesis: ( m + n = 0 implies P1[m,n] )
assume m + n = 0 ; :: thesis: P1[m,n]
then m = 0 ;
hence P1[m,n] by A1; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A8, A3);
 then S1[k] ;
hence P1[n,m] ; :: thesis: verum