defpred S₁[ Nat] means for m, n being natural number st m + n = $1 holds
P₁[m,n];
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
for m, n being natural number st m + n = k + 1 holds
P₁[m,n]

proof

let m, n be natural number ; :: thesis: ( m + n = k + 1 implies P₁[m,n] )
assume A5: m + n = k + 1 ; :: thesis: P₁[m,n]

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

suppose ( m = 0 or n = 0 ) ; :: thesis: P₁[m,n]

hence P₁[m,n] by A1; :: thesis: verum

end;

suppose A6: ( m <> 0 & n <> 0 ) ; :: thesis: P₁[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₁[m9,n9 + 1] by A4;
m + n9 = k by A5;
then P₁[m9 + 1,n9] by A4;
hence P₁[m,n] by A2, A7; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

let m, n be natural number ; :: thesis: P₁[m,n]
set k = m + n;
reconsider k = m + n as Element of NAT by ORDINAL1:def 12;
A8: S₁[ 0 ]

proof

let m, n be natural number ; :: thesis: ( m + n = 0 implies P₁[m,n] )
assume m + n = 0 ; :: thesis: P₁[m,n]
then m = 0 ;
hence P₁[m,n] by A1; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A8, A3);
then S₁[k] ;
hence P₁[m,n] ; :: thesis: verum