defpred S₁[ Nat] means for m, n being natural number st m + n = $1 holds
P₁[m,n];
A3: 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 & n = 0 ) ;
hence P₁[m,n] by A1; :: thesis: verum

end;

A4: 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 A5: 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 A6: 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 A7: ( m <> 0 & n <> 0 ) ; :: thesis: P₁[m,n]

then reconsider n' = n - 1 as Element of NAT by NAT_1:20;
A8: m + n' = k by A6;
reconsider m' = m - 1 as Element of NAT by A7, NAT_1:20;
m' + n = k by A6;
then ( P₁[m',n' + 1] & P₁[m' + 1,n'] ) by A5, A8;
hence P₁[m,n] by A2; :: thesis: verum

end;

end;

end;

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

end;

A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
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 13;
S₁[k] by A9;
hence P₁[m,n] ; :: thesis: verum