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: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A3: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
let n, m be Nat; :: thesis: ( n + m = k implies (uInt . n) * (uInt . m) == uInt . (n * m) )
assume A4: n + m = k ; :: 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, nm1 = (n * m) - 1 as Nat by NAT_1:20;
A5: ( uInt . (n1 + 1) = [{(uInt . n1)},{}] & uInt . (m1 + 1) = [{(uInt . m1)},{}] ) by Def1;
A6: uInt . (nm1 + 1) = [{(uInt . nm1)},{}] by Def1;
set x = uInt . n;
set y = uInt . m;
reconsider nm1 = (n * m) - 1 as Nat by A6;
comp ((R_ (uInt . n)),(uInt . n),(uInt . m),(L_ (uInt . m))) = comp ((L_ (uInt . m)),(uInt . m),(uInt . n),(R_ (uInt . n))) by SURREALR:53;
then A7: comp ((R_ (uInt . n)),(uInt . n),(uInt . m),(L_ (uInt . m))) = {} by A5, SURREALR:49;
A8: ( comp ((L_ (uInt . n)),(uInt . n),(uInt . m),(R_ (uInt . m))) = {} & {} = comp ((R_ (uInt . n)),(uInt . n),(uInt . m),(R_ (uInt . m))) ) by A5, SURREALR:49;
A9: ( n1 < n1 + 1 & m1 < m1 + 1 ) by NAT_1:13;
then A10: ( n1 + m < n + m & n1 + m1 < n + m1 & n + m1 < n + m ) by XREAL_1:8;
n1 + m1 < n + m by A9, XREAL_1:8;
then ( (uInt . n1) * (uInt . m) == uInt . (n1 * m) & (uInt . n1) * (uInt . m1) == uInt . (n1 * m1) & (uInt . n) * (uInt . m1) == uInt . (n * m1) ) by A4, A3, A10;
then ( ((uInt . n1) * (uInt . m)) + ((uInt . n) * (uInt . m1)) == (uInt . (n1 * m)) + (uInt . (n * m1)) & (uInt . (n1 * m)) + (uInt . (n * m1)) = uInt . ((n1 * m) + (n * m1)) & - ((uInt . n1) * (uInt . m1)) == - (uInt . (n1 * m1)) & - (uInt . (n1 * m1)) = uInt . (- (n1 * m1)) ) by Th13, SURREALR:10, SURREALR:43, Th12;
then ( (((uInt . n1) * (uInt . m)) + ((uInt . n) * (uInt . m1))) + (- ((uInt . n1) * (uInt . m1))) == (uInt . ((n1 * m) + (n * m1))) + (uInt . (- (n1 * m1))) & (uInt . ((n1 * m) + (n * m1))) + (uInt . (- (n1 * m1))) == uInt . (((n1 * m) + (n * m1)) + (- (n1 * m1))) ) by Th14, SURREALR:43;
then (((uInt . n1) * (uInt . m)) + ((uInt . n) * (uInt . m1))) + (- ((uInt . n1) * (uInt . m1))) == uInt . nm1 by SURREALO:4;
then {((((uInt . n1) * (uInt . m)) + ((uInt . n) * (uInt . m1))) - ((uInt . n1) * (uInt . m1)))} <==> {(uInt . nm1)} by SURREALO:32;
then A11: comp ((L_ (uInt . n)),(uInt . n),(uInt . m),(L_ (uInt . m))) <==> {(uInt . nm1)} by A5, SURREALR:52;
(uInt . n) * (uInt . m) = [((comp ((L_ (uInt . n)),(uInt . n),(uInt . m),(L_ (uInt . m)))) \/ {}),({} \/ {})] by A7, A8, SURREALR:50
.= [(comp ((L_ (uInt . n)),(uInt . n),(uInt . m),(L_ (uInt . m)))),{}] ;
hence (uInt . n) * (uInt . m) == uInt . (n * m) by A6, A11, SURREALO:29; :: thesis: verum

end;

end;

end;

A12: for k being Nat holds S₁[k] from NAT_1:sch 4(A2);
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
A13: ( 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
A14: ( j = n or j = - n ) by INT_1:def 1;
A15: S₁[n + k] by A12;
then A16: (uInt . n) * (uInt . k) == uInt . (n * k) ;

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

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

hence (uInt . i) * (uInt . j) == uInt . (i * j) by A15; :: thesis: verum

end;

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

(uInt . n) * (uInt . (- k)) = (uInt . n) * (- (uInt . k)) by Th12
.= - ((uInt . n) * (uInt . k)) by SURREALR:58 ;
then (uInt . n) * (uInt . (- k)) == - (uInt . (n * k)) by A16, SURREALR:10;
then (uInt . n) * (uInt . (- k)) == uInt . (- (n * k)) by Th12;
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)

(uInt . (- n)) * (uInt . k) = (- (uInt . n)) * (uInt . k) by Th12
.= - ((uInt . n) * (uInt . k)) by SURREALR:58 ;
then (uInt . (- n)) * (uInt . k) == - (uInt . (n * k)) by A16, SURREALR:10;
then (uInt . (- n)) * (uInt . k) == uInt . (- (n * k)) by Th12;
hence (uInt . i) * (uInt . j) == uInt . (i * j) by A18; :: thesis: verum

end;

suppose A19: ( i = - k & j = - n ) ; :: thesis: (uInt . i) * (uInt . j) == uInt . (i * j)

(uInt . (- n)) * (uInt . (- k)) = (- (uInt . n)) * (uInt . (- k)) by Th12
.= (- (uInt . n)) * (- (uInt . k)) by Th12
.= - (- ((uInt . n) * (uInt . k))) by SURREALR:58
.= (uInt . n) * (uInt . k) ;
hence (uInt . i) * (uInt . j) == uInt . (i * j) by A19, A16; :: thesis: verum

end;

end;