let n, m be Nat; :: thesis: (uInt . n) + (uInt . m) = uInt . (n + m)
defpred S₁[ Nat] means (uInt . $1) + 1_No = uInt . ($1 + 1);
A1: ( uInt . 0 = 0_No & uInt . 1 = 1_No ) by Def1, Th11;
then A2: S₁[ 0 ] ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set s = uInt . (n + 1);
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
A5: {(uInt . (n + 1))} ++ (L_ 1_No) = {((uInt . (n + 1)) + 0_No)} by SURREALR:36;
R_ (uInt . (n + 1)) = {} by Th7;
then A6: (R_ (uInt . (n + 1))) ++ {1_No} = {} by SURREALR:27;
uInt . (n + 1) = [{(uInt . n)},{}] by Def1;
then A7: (L_ (uInt . (n + 1))) ++ {1_No} = {(uInt . (n + 1))} by A4, SURREALR:36;
thus (uInt . (n + 1)) + 1_No = [(((L_ (uInt . (n + 1))) ++ {1_No}) \/ ({(uInt . (n + 1))} ++ (L_ 1_No))),(((R_ (uInt . (n + 1))) ++ {1_No}) \/ ({(uInt . (n + 1))} ++ (R_ 1_No)))] by SURREALR:28
.= [({(uInt . (n + 1))} \/ {(uInt . (n + 1))}),({} \/ {})] by A5, SURREALR:27, A6, A7
.= uInt . ((n + 1) + 1) by Def1 ; :: thesis: verum

end;

A8: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
defpred S₂[ Nat] means (uInt . n) + (uInt . $1) = uInt . (n + $1);
A9: S₂[ 0 ] by A1;
A10: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A11: S₂[m] ; :: thesis: S₂[m + 1]
(uInt . n) + (uInt . (m + 1)) = (uInt . n) + ((uInt . m) + (uInt . 1)) by Th11, A8
.= (uInt . (n + m)) + 1_No by Th11, A11, SURREALR:37
.= uInt . ((n + m) + 1) by A8 ;
hence S₂[m + 1] ; :: thesis: verum

end;

for m being Nat holds S₂[m] from NAT_1:sch 2(A9, A10);
hence (uInt . n) + (uInt . m) = uInt . (n + m) ; :: thesis: verum