let n, m be Element of NAT ; :: thesis: n + m = n +^ m
defpred S₁[ Element of NAT ] means n + $1 = n +^ $1;
A1: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
thus n + (m + 1) = (n + m) + 1
.= succ (n +^ m) by A2, NAT_1:39
.= n +^ (succ m) by ORDINAL2:45
.= n +^ (m + 1) by NAT_1:39 ; :: thesis: verum

end;

A3: S₁[ 0 ] by ORDINAL2:44;
for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A3, A1);
hence n + m = n +^ m ; :: thesis: verum