A1: uInt . 0 = 0_No by Def1;
defpred S₁[ Nat] means for n, m being Nat st n + m = $1 holds
(uInt . n) + (uInt . (- m)) == uInt . (n - m);
A2: S₁[ 0 ]

proof

let n, m be Nat; :: thesis: ( n + m = 0 implies (uInt . n) + (uInt . (- m)) == uInt . (n - m) )
assume n + m = 0 ; :: thesis: (uInt . n) + (uInt . (- m)) == uInt . (n - m)
then ( n = 0 & m = 0 ) ;
hence (uInt . n) + (uInt . (- m)) == uInt . (n - m) by A1; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let n, m be Nat; :: thesis: ( n + m = k + 1 implies (uInt . n) + (uInt . (- m)) == uInt . (n - m) )
assume A5: n + m = k + 1 ; :: thesis: (uInt . n) + (uInt . (- m)) == uInt . (n - m)

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

suppose ( n = 0 or m = 0 ) ; :: thesis: (uInt . n) + (uInt . (- m)) == uInt . (n - m)

hence (uInt . n) + (uInt . (- m)) == uInt . (n - m) by A1; :: thesis: verum

end;

suppose ( n <> 0 & m <> 0 ) ; :: thesis: (uInt . n) + (uInt . (- m)) == uInt . (n - m)

then reconsider n1 = n - 1, m1 = m - 1 as Nat by NAT_1:20;
A6: ( uInt . (n1 + 1) = [{(uInt . n1)},{}] & uInt . (- (m1 + 1)) = [{},{(uInt . (- m1))}] ) by Def1;
then A7: ( {(uInt . n)} ++ (L_ (uInt . (- m))) = {} & {} = (R_ (uInt . n)) ++ {(uInt . (- m))} ) by SURREALR:27;
n1 + m = k by A5;
then A8: (uInt . n1) + (uInt . (- m)) == uInt . (n1 - m) by A4;
(L_ (uInt . n)) ++ {(uInt . (- m))} = {((uInt . n1) + (uInt . (- m)))} by SURREALR:36, A6;
then A9: (L_ (uInt . n)) ++ {(uInt . (- m))} <==> {(uInt . ((n - m) - 1))} by A8, SURREALO:32;
n + m1 = k by A5;
then A10: (uInt . n) + (uInt . (- m1)) == uInt . (n - m1) by A4;
{(uInt . n)} ++ (R_ (uInt . (- m))) = {((uInt . n) + (uInt . (- m1)))} by A6, SURREALR:36;
then A11: {(uInt . n)} ++ (R_ (uInt . (- m))) <==> {(uInt . ((n - m) + 1))} by A10, SURREALO:32;
reconsider ss = [{(uInt . ((n - m) - 1))},{(uInt . ((n - m) + 1))}] as Surreal by Th10;
A12: ss == uInt . (n - m) by Th10;
(uInt . n) + (uInt . (- m)) = [(((L_ (uInt . n)) ++ {(uInt . (- m))}) \/ {}),({} \/ ({(uInt . n)} ++ (R_ (uInt . (- m)))))] by A7, SURREALR:28
.= [((L_ (uInt . n)) ++ {(uInt . (- m))}),({(uInt . n)} ++ (R_ (uInt . (- m))))] ;
then (uInt . n) + (uInt . (- m)) == ss by A9, A11, SURREALO:29;
hence (uInt . n) + (uInt . (- m)) == uInt . (n - m) by A12, SURREALO:4; :: thesis: verum

end;

end;

end;

A13: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
let i, j be Integer; :: thesis: (uInt . i) + (uInt . j) == uInt . (i + j)
i in INT by INT_1:def 2;
then consider k being Nat such that
A14: ( i = k or i = - k ) by INT_1:def 1;
j in INT by INT_1:def 2;
then consider n being Nat such that
A15: ( j = n or j = - n ) by INT_1:def 1;

per cases ( ( i = k & j = n ) or ( i = - k & j = n ) or ( i = k & j = - n ) or ( i = - k & j = - n ) ) by A14, A15;

suppose ( i = k & j = n ) ; :: thesis: (uInt . i) + (uInt . j) == uInt . (i + j)

hence (uInt . i) + (uInt . j) == uInt . (i + j) by Th13; :: thesis: verum

end;

suppose A16: ( i = - k & j = n ) ; :: thesis: (uInt . i) + (uInt . j) == uInt . (i + j)

S₁[n + k] by A13;
then (uInt . n) + (uInt . (- k)) == uInt . (n - k) ;
hence (uInt . i) + (uInt . j) == uInt . (i + j) by A16; :: thesis: verum

end;

suppose A17: ( i = k & j = - n ) ; :: thesis: (uInt . i) + (uInt . j) == uInt . (i + j)

S₁[k + n] by A13;
then (uInt . k) + (uInt . (- n)) == uInt . (k - n) ;
hence (uInt . i) + (uInt . j) == uInt . (i + j) by A17; :: thesis: verum

end;

suppose A18: ( i = - k & j = - n ) ; :: thesis: (uInt . i) + (uInt . j) == uInt . (i + j)

then (uInt . i) + (uInt . j) = (- (uInt . k)) + (uInt . (- n)) by Th12
.= (- (uInt . k)) + (- (uInt . n)) by Th12
.= - ((uInt . k) + (uInt . n)) by SURREALR:40
.= - (uInt . (k + n)) by Th13
.= uInt . (- (k + n)) by Th12 ;
hence (uInt . i) + (uInt . j) == uInt . (i + j) by A18; :: thesis: verum

end;

end;