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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
thus n + (m + 1) = Segm ((n + m) + 1)
.= succ (Segm (n + m)) by NAT_1:38
.= succ (n +^ m) by A2
.= n +^ (succ (Segm m)) by ORDINAL2:28
.= n +^ (Segm (m + 1)) by NAT_1:38
.= n +^ (m + 1) ; :: thesis: verum

end;

A3: S₁[ 0 ] by ORDINAL2:27;
for m being Nat holds S₁[m] from NAT_1:sch 2(A3, A1);
hence n + m = n +^ m ; :: thesis: verum