let d1, d2 be Dyadic; :: thesis: (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)
defpred S₁[ Nat] means for n1, n2 being Nat st n1 + n2 <= $1 & n1 <= n2 holds
for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2);
A1: S₁[ 0 ]

proof

let n1, n2 be Nat; :: thesis: ( n1 + n2 <= 0 & n1 <= n2 implies for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) )
assume A2: ( n1 + n2 <= 0 & n1 <= n2 ) ; :: thesis: for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)
A3: ( n1 = 0 & 0 = n2 ) by A2;
let d1, d2 be Dyadic; :: thesis: ( d1 in DYADIC n1 & d2 in DYADIC n2 implies (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) )
assume A4: ( d1 in DYADIC n1 & d2 in DYADIC n2 ) ; :: thesis: (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)
reconsider i1 = d1, i2 = d2 as Integer by A4, A3, Th21;
( uDyadic . d1 = uInt . i1 & uDyadic . d2 = uInt . i2 & uDyadic . (d1 * d2) = uInt . (i1 * i2) ) by Def5;
hence (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) by Th15; :: thesis: verum

end;

A5: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A6: S₁[m] ; :: thesis: S₁[m + 1]
set m1 = m + 1;
let n1, n2 be Nat; :: thesis: ( n1 + n2 <= m + 1 & n1 <= n2 implies for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) )
assume A7: ( n1 + n2 <= m + 1 & n1 <= n2 ) ; :: thesis: for d1, d2 being Dyadic st d1 in DYADIC n1 & d2 in DYADIC n2 holds
(uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)
let d1, d2 be Dyadic; :: thesis: ( d1 in DYADIC n1 & d2 in DYADIC n2 implies (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) )
assume A8: ( d1 in DYADIC n1 & d2 in DYADIC n2 ) ; :: thesis: (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)

per cases ( n1 = 0 or n1 <> 0 ) ;

suppose n1 = 0 ; :: thesis: (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)

then reconsider i1 = d1 as Integer by A8, Th21;
(uDyadic . i1) * (uDyadic . d2) == uDyadic . (i1 * d2) by Lm9;
hence (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) ; :: thesis: verum

end;

suppose A9: n1 <> 0 ; :: thesis: (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)

then reconsider N1 = n1 - 1 as Nat by NAT_1:20;
A10: (N1 + n2) + 1 <= m + 1 by A7;
then A11: N1 + n2 <= m by XREAL_1:6;
n2 <> 0 by A7, A9;
then reconsider N2 = n2 - 1 as Nat by NAT_1:20;
A12: N1 + n2 = n1 + N2 ;
(N1 + N2) + 1 <= m by A10, XREAL_1:6;
then A13: N1 + N2 < m by NAT_1:13;
N1 + 1 <= n2 by A7;
then ( N1 < n2 & n2 = N2 + 1 ) by NAT_1:13;
then A14: N1 <= N2 by NAT_1:13;
A15: ( ( N1 <= n2 or n2 <= N1 ) & ( n1 <= N2 or N2 <= n1 ) ) ;

per cases ( d1 in DYADIC N1 or d2 in DYADIC N2 or ( not d1 in DYADIC N1 & not d2 in DYADIC N2 ) ) ;

suppose ( d1 in DYADIC N1 or d2 in DYADIC N2 ) ; :: thesis: (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)

hence (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) by A12, A11, A8, A6, A15; :: thesis: verum

end;

suppose A16: ( not d1 in DYADIC N1 & not d2 in DYADIC N2 ) ; :: thesis: (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)

then d1 in (DYADIC (N1 + 1)) \ (DYADIC N1) by A8, XBOOLE_0:def 5;
then consider i1 being Integer such that
A17: d1 = ((2 * i1) + 1) / (2 |^ (N1 + 1)) by Th20;
d2 in (DYADIC (N2 + 1)) \ (DYADIC N2) by A8, A16, XBOOLE_0:def 5;
then consider i2 being Integer such that
A18: d2 = ((2 * i2) + 1) / (2 |^ (N2 + 1)) by Th20;
A19: uDyadic . d1 = [{(uDyadic . (i1 / (2 |^ N1)))},{(uDyadic . ((i1 + 1) / (2 |^ N1)))}] by A17, Def5;
A20: uDyadic . d2 = [{(uDyadic . (i2 / (2 |^ N2)))},{(uDyadic . ((i2 + 1) / (2 |^ N2)))}] by A18, Def5;
set x = uDyadic . d1;
set y = uDyadic . d2;
A21: ( i1 / (2 |^ N1) in DYADIC N1 & (i1 + 1) / (2 |^ N1) in DYADIC N1 & i2 / (2 |^ N2) in DYADIC N2 & (i2 + 1) / (2 |^ N2) in DYADIC N2 ) by Def4;
A22: (uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2) == uDyadic . ((i1 / (2 |^ N1)) * d2) by A21, A11, A8, A6, A15;
A23: (uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))) == uDyadic . (d1 * (i2 / (2 |^ N2))) by A21, A12, A11, A8, A6, A15;
A24: (uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2) == uDyadic . (((i1 + 1) / (2 |^ N1)) * d2) by A21, A11, A8, A6, A15;
A25: (uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))) == uDyadic . (d1 * ((i2 + 1) / (2 |^ N2))) by A21, A12, A11, A8, A6, A15;
A26: ( 2 |^ (N1 + 1) = 2 * (2 |^ N1) & 2 |^ (N2 + 1) = 2 * (2 |^ N2) ) by NEWTON:6;
set M = 2 |^ ((N1 + N2) + 1);
A27: 2 |^ ((N1 + N2) + 1) = (2 |^ (N1 + N2)) * 2 by NEWTON:6
.= ((2 |^ N1) * (2 |^ N2)) * 2 by NEWTON:8 ;
A28: (i1 / (2 |^ N1)) * d2 = (i1 * ((2 * i2) + 1)) / ((2 |^ N1) * (2 |^ (N2 + 1))) by XCMPLX_1:76, A18
.= (((2 * i1) * i2) + i1) / (2 |^ ((N1 + N2) + 1)) by A27, A26 ;
A29: d1 * (i2 / (2 |^ N2)) = (((2 * i1) + 1) * i2) / ((2 |^ (N1 + 1)) * (2 |^ N2)) by XCMPLX_1:76, A17
.= (((2 * i1) * i2) + i2) / (2 |^ ((N1 + N2) + 1)) by A27, A26 ;
A30: (i1 / (2 |^ N1)) * (i2 / (2 |^ N2)) = (i1 * i2) / ((2 |^ N1) * (2 |^ N2)) by XCMPLX_1:76
.= ((i1 * i2) * 2) / (2 |^ ((N1 + N2) + 1)) by A27, XCMPLX_1:91 ;
A31: ((i1 + 1) / (2 |^ N1)) * d2 = ((i1 + 1) * ((2 * i2) + 1)) / ((2 |^ N1) * (2 |^ (N2 + 1))) by XCMPLX_1:76, A18
.= (((((2 * i1) * i2) + i1) + (2 * i2)) + 1) / (2 |^ ((N1 + N2) + 1)) by A27, A26 ;
A32: d1 * ((i2 + 1) / (2 |^ N2)) = (((2 * i1) + 1) * (i2 + 1)) / ((2 |^ (N1 + 1)) * (2 |^ N2)) by XCMPLX_1:76, A17
.= (((((2 * i1) * i2) + i2) + (2 * i1)) + 1) / (2 |^ ((N1 + N2) + 1)) by A27, A26 ;
A33: ((i1 + 1) / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)) = ((i1 + 1) * (i2 + 1)) / ((2 |^ N1) * (2 |^ N2)) by XCMPLX_1:76
.= (((((i1 * i2) + i1) + i2) + 1) * 2) / (2 |^ ((N1 + N2) + 1)) by A27, XCMPLX_1:91 ;
A34: (i1 / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)) = (i1 * (i2 + 1)) / ((2 |^ N1) * (2 |^ N2)) by XCMPLX_1:76
.= (((i1 * i2) + i1) * 2) / (2 |^ ((N1 + N2) + 1)) by A27, XCMPLX_1:91 ;
A35: ((i1 + 1) / (2 |^ N1)) * (i2 / (2 |^ N2)) = ((i1 + 1) * i2) / ((2 |^ N1) * (2 |^ N2)) by XCMPLX_1:76
.= (((i1 * i2) + i2) * 2) / (2 |^ ((N1 + N2) + 1)) by A27, XCMPLX_1:91 ;
A36: (((i1 / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2)))) + (- ((i1 / (2 |^ N1)) * (i2 / (2 |^ N2)))) = (((((2 * i1) * i2) + i1) + (((2 * i1) * i2) + i2)) / (2 |^ ((N1 + N2) + 1))) + (- (((i1 * i2) * 2) / (2 |^ ((N1 + N2) + 1)))) by A28, A29, A30, XCMPLX_1:62
.= (((((2 * i1) * i2) + i1) + (((2 * i1) * i2) + i2)) / (2 |^ ((N1 + N2) + 1))) - (((i1 * i2) * 2) / (2 |^ ((N1 + N2) + 1)))
.= (((((2 * i1) * i2) + i1) + (((2 * i1) * i2) + i2)) - ((i1 * i2) * 2)) / (2 |^ ((N1 + N2) + 1)) by XCMPLX_1:120
.= (((2 * i1) * i2) + (i1 + i2)) / (2 |^ ((N1 + N2) + 1)) ;
A37: ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2)))) + (- (((i1 + 1) / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)))) = (((((((2 * i1) * i2) + i1) + (2 * i2)) + 1) + (((((2 * i1) * i2) + i2) + (2 * i1)) + 1)) / (2 |^ ((N1 + N2) + 1))) + (- ((((((i1 * i2) + i1) + i2) + 1) * 2) / (2 |^ ((N1 + N2) + 1)))) by A31, A32, A33, XCMPLX_1:62
.= ((((((4 * i1) * i2) + (3 * i1)) + (3 * i2)) + 2) / (2 |^ ((N1 + N2) + 1))) - ((((((i1 * i2) + i1) + i2) + 1) * 2) / (2 |^ ((N1 + N2) + 1)))
.= ((((((4 * i1) * i2) + (3 * i1)) + (3 * i2)) + 2) - (((((i1 * i2) + i1) + i2) + 1) * 2)) / (2 |^ ((N1 + N2) + 1)) by XCMPLX_1:120
.= ((((2 * i1) * i2) + i1) + i2) / (2 |^ ((N1 + N2) + 1)) ;
A38: (((i1 / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2)))) + (- ((i1 / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)))) = (((((2 * i1) * i2) + i1) + (((((2 * i1) * i2) + i2) + (2 * i1)) + 1)) / (2 |^ ((N1 + N2) + 1))) + (- ((((i1 * i2) + i1) * 2) / (2 |^ ((N1 + N2) + 1)))) by A34, A28, A32, XCMPLX_1:62
.= ((((((4 * i1) * i2) + (3 * i1)) + i2) + 1) / (2 |^ ((N1 + N2) + 1))) - ((((i1 * i2) + i1) * 2) / (2 |^ ((N1 + N2) + 1)))
.= ((((((4 * i1) * i2) + (3 * i1)) + i2) + 1) - (((i1 * i2) + i1) * 2)) / (2 |^ ((N1 + N2) + 1)) by XCMPLX_1:120
.= (((((2 * i1) * i2) + i1) + i2) + 1) / (2 |^ ((N1 + N2) + 1)) ;
A39: ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2)))) + (- (((i1 + 1) / (2 |^ N1)) * (i2 / (2 |^ N2)))) = (((((((2 * i1) * i2) + i1) + (2 * i2)) + 1) + (((2 * i1) * i2) + i2)) / (2 |^ ((N1 + N2) + 1))) + (- ((((i1 * i2) + i2) * 2) / (2 |^ ((N1 + N2) + 1)))) by A35, A29, A31, XCMPLX_1:62
.= ((((((4 * i1) * i2) + i1) + (3 * i2)) + 1) / (2 |^ ((N1 + N2) + 1))) - ((((i1 * i2) + i2) * 2) / (2 |^ ((N1 + N2) + 1)))
.= ((((((4 * i1) * i2) + i1) + (3 * i2)) + 1) - (((i1 * i2) + i2) * 2)) / (2 |^ ((N1 + N2) + 1)) by XCMPLX_1:120
.= (((((2 * i1) * i2) + i1) + i2) + 1) / (2 |^ ((N1 + N2) + 1)) ;
( ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2)))) == (uDyadic . ((i1 / (2 |^ N1)) * d2)) + (uDyadic . (d1 * (i2 / (2 |^ N2)))) & (uDyadic . ((i1 / (2 |^ N1)) * d2)) + (uDyadic . (d1 * (i2 / (2 |^ N2)))) == uDyadic . (((i1 / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2)))) ) by SURREALR:43, Th39, A22, A23;
then A40: ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2)))) == uDyadic . (((i1 / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2)))) by SURREALO:4;
( - ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2)))) == - (uDyadic . ((i1 / (2 |^ N1)) * (i2 / (2 |^ N2)))) & - (uDyadic . ((i1 / (2 |^ N1)) * (i2 / (2 |^ N2)))) = uDyadic . (- ((i1 / (2 |^ N1)) * (i2 / (2 |^ N2)))) ) by A14, A13, A21, A6, SURREALR:65, Th27;
then ( (((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2))))) == (uDyadic . (((i1 / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2))))) + (uDyadic . (- ((i1 / (2 |^ N1)) * (i2 / (2 |^ N2))))) & (uDyadic . (((i1 / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2))))) + (uDyadic . (- ((i1 / (2 |^ N1)) * (i2 / (2 |^ N2))))) == uDyadic . ((((i1 / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2)))) + (- ((i1 / (2 |^ N1)) * (i2 / (2 |^ N2))))) ) by A40, SURREALR:43, Th39;
then A41: (((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2))))) == uDyadic . ((((2 * i1) * i2) + (i1 + i2)) / (2 |^ ((N1 + N2) + 1))) by SURREALO:4, A36;
then A42: {((((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2))))))} <==> {(uDyadic . ((((2 * i1) * i2) + (i1 + i2)) / (2 |^ ((N1 + N2) + 1))))} by SURREALO:32;
A43: comp ((L_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(L_ (uDyadic . d2))) = {((((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) - ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2)))))} by A19, A20, SURREALR:52;
( ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2)))) == (uDyadic . (((i1 + 1) / (2 |^ N1)) * d2)) + (uDyadic . (d1 * ((i2 + 1) / (2 |^ N2)))) & (uDyadic . (((i1 + 1) / (2 |^ N1)) * d2)) + (uDyadic . (d1 * ((i2 + 1) / (2 |^ N2)))) == uDyadic . ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2)))) ) by SURREALR:43, Th39, A24, A25;
then A44: ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2)))) == uDyadic . ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2)))) by SURREALO:4;
( - ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2)))) == - (uDyadic . (((i1 + 1) / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)))) & - (uDyadic . (((i1 + 1) / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)))) = uDyadic . (- (((i1 + 1) / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)))) ) by A14, A13, A21, A6, SURREALR:65, Th27;
then ( (((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) + (- ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) == (uDyadic . ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2))))) + (uDyadic . (- (((i1 + 1) / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2))))) & (uDyadic . ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2))))) + (uDyadic . (- (((i1 + 1) / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2))))) == uDyadic . (((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2)))) + (- (((i1 + 1) / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2))))) ) by A44, SURREALR:43, Th39;
then A45: (((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) + (- ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) == uDyadic . (((((2 * i1) * i2) + i1) + i2) / (2 |^ ((N1 + N2) + 1))) by SURREALO:4, A37;
A46: comp ((R_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(R_ (uDyadic . d2))) = {((((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) - ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2)))))} by A19, A20, SURREALR:52;
( ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2)))) == (uDyadic . ((i1 / (2 |^ N1)) * d2)) + (uDyadic . (d1 * ((i2 + 1) / (2 |^ N2)))) & (uDyadic . ((i1 / (2 |^ N1)) * d2)) + (uDyadic . (d1 * ((i2 + 1) / (2 |^ N2)))) == uDyadic . (((i1 / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2)))) ) by SURREALR:43, Th39, A22, A25;
then A47: ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2)))) == uDyadic . (((i1 / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2)))) by SURREALO:4;
( - ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2)))) == - (uDyadic . ((i1 / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)))) & - (uDyadic . ((i1 / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)))) = uDyadic . (- ((i1 / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2)))) ) by A14, A13, A21, A6, SURREALR:65, Th27;
then ( (((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) == (uDyadic . (((i1 / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2))))) + (uDyadic . (- ((i1 / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2))))) & (uDyadic . (((i1 / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2))))) + (uDyadic . (- ((i1 / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2))))) == uDyadic . ((((i1 / (2 |^ N1)) * d2) + (d1 * ((i2 + 1) / (2 |^ N2)))) + (- ((i1 / (2 |^ N1)) * ((i2 + 1) / (2 |^ N2))))) ) by A47, SURREALR:43, Th39;
then A48: (((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) == uDyadic . ((((((2 * i1) * i2) + i1) + i2) + 1) / (2 |^ ((N1 + N2) + 1))) by SURREALO:4, A38;
then A49: {((((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2))))))} <==> {(uDyadic . ((((((2 * i1) * i2) + i1) + i2) + 1) / (2 |^ ((N1 + N2) + 1))))} by SURREALO:32;
A50: comp ((L_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(R_ (uDyadic . d2))) = {((((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) - ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2)))))} by SURREALR:52, A19, A20;
( ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2)))) == (uDyadic . (((i1 + 1) / (2 |^ N1)) * d2)) + (uDyadic . (d1 * (i2 / (2 |^ N2)))) & (uDyadic . (((i1 + 1) / (2 |^ N1)) * d2)) + (uDyadic . (d1 * (i2 / (2 |^ N2)))) == uDyadic . ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2)))) ) by SURREALR:43, Th39, A23, A24;
then A51: ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2)))) == uDyadic . ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2)))) by SURREALO:4;
( - ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2)))) == - (uDyadic . (((i1 + 1) / (2 |^ N1)) * (i2 / (2 |^ N2)))) & - (uDyadic . (((i1 + 1) / (2 |^ N1)) * (i2 / (2 |^ N2)))) = uDyadic . (- (((i1 + 1) / (2 |^ N1)) * (i2 / (2 |^ N2)))) ) by A14, A13, A21, A6, SURREALR:65, Th27;
then ( (((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) + (- ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2))))) == (uDyadic . ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2))))) + (uDyadic . (- (((i1 + 1) / (2 |^ N1)) * (i2 / (2 |^ N2))))) & (uDyadic . ((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2))))) + (uDyadic . (- (((i1 + 1) / (2 |^ N1)) * (i2 / (2 |^ N2))))) == uDyadic . (((((i1 + 1) / (2 |^ N1)) * d2) + (d1 * (i2 / (2 |^ N2)))) + (- (((i1 + 1) / (2 |^ N1)) * (i2 / (2 |^ N2))))) ) by A51, SURREALR:43, Th39;
then A52: (((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) + (- ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2))))) == uDyadic . ((((((2 * i1) * i2) + i1) + i2) + 1) / (2 |^ ((N1 + N2) + 1))) by SURREALO:4, A39;
A53: comp ((R_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(L_ (uDyadic . d2))) = {((((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) - ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2)))))} by SURREALR:52, A19, A20;
A54: (uDyadic . d1) * (uDyadic . d2) = [((comp ((L_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(L_ (uDyadic . d2)))) \/ (comp ((R_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(R_ (uDyadic . d2))))),((comp ((L_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(R_ (uDyadic . d2)))) \/ (comp ((R_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(L_ (uDyadic . d2)))))] by SURREALR:50
.= [{((((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2)))))),((((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) + (- ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2))))))},((comp ((L_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(R_ (uDyadic . d2)))) \/ (comp ((R_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(L_ (uDyadic . d2)))))] by A43, A46, ENUMSET1:1 ;
then reconsider DD1 = [{((((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2))))))},((comp ((L_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(R_ (uDyadic . d2)))) \/ (comp ((R_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(L_ (uDyadic . d2)))))] as Surreal by SURREALO:26;
A55: (uDyadic . d1) * (uDyadic . d2) == DD1 by A54, SURREALO:4, SURREALO:25, A41, A45;
then reconsider DD2 = [{(uDyadic . (((((2 * i1) * i2) + i1) + i2) / (2 |^ ((N1 + N2) + 1))))},((comp ((L_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(R_ (uDyadic . d2)))) \/ (comp ((R_ (uDyadic . d1)),(uDyadic . d1),(uDyadic . d2),(L_ (uDyadic . d2)))))] as Surreal by A42, SURREALI:37, TARSKI:1;
A56: DD1 == DD2 by A42, SURREALO:29;
A57: DD2 = [{(uDyadic . (((((2 * i1) * i2) + i1) + i2) / (2 |^ ((N1 + N2) + 1))))},{((((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2)))))),((((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . (i2 / (2 |^ N2))))) + (- ((uDyadic . ((i1 + 1) / (2 |^ N1))) * (uDyadic . (i2 / (2 |^ N2))))))}] by A50, A53, ENUMSET1:1;
then reconsider DD3 = [{(uDyadic . (((((2 * i1) * i2) + i1) + i2) / (2 |^ ((N1 + N2) + 1))))},{((((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . d2)) + ((uDyadic . d1) * (uDyadic . ((i2 + 1) / (2 |^ N2))))) + (- ((uDyadic . (i1 / (2 |^ N1))) * (uDyadic . ((i2 + 1) / (2 |^ N2))))))}] as Surreal by SURREALO:28;
A58: DD2 == DD3 by A57, SURREALO:4, SURREALO:27, A48, A52;
then reconsider DD4 = [{(uDyadic . (((((2 * i1) * i2) + i1) + i2) / (2 |^ ((N1 + N2) + 1))))},{(uDyadic . ((((((2 * i1) * i2) + i1) + i2) + 1) / (2 |^ ((N1 + N2) + 1))))}] as Surreal by A49, SURREALI:37, TARSKI:1;
(uDyadic . d1) * (uDyadic . d2) == DD2 by A55, A56, SURREALO:4;
then A59: (uDyadic . d1) * (uDyadic . d2) == DD3 by A58, SURREALO:4;
DD3 == DD4 by A49, SURREALO:29;
then A60: (uDyadic . d1) * (uDyadic . d2) == DD4 by A59, SURREALO:4;
A61: 2 * (2 |^ ((N1 + N2) + 1)) = 2 |^ (((N1 + N2) + 1) + 1) by NEWTON:6;
A62: ((((2 * i1) * i2) + i1) + i2) / (2 |^ ((N1 + N2) + 1)) = (((((2 * i1) * i2) + i1) + i2) * 2) / (2 * (2 |^ ((N1 + N2) + 1))) by XCMPLX_1:91;
(((((2 * i1) * i2) + i1) + i2) + 1) / (2 |^ ((N1 + N2) + 1)) = ((((((2 * i1) * i2) + i1) + i2) + 1) * 2) / (2 * (2 |^ ((N1 + N2) + 1))) by XCMPLX_1:91
.= ((((((2 * i1) * i2) + i1) + i2) * 2) + 2) / (2 * (2 |^ ((N1 + N2) + 1))) ;
then A63: DD4 == uDyadic . (((((((2 * i1) * i2) + i1) + i2) * 2) + 1) / (2 |^ (((N1 + N2) + 1) + 1))) by A61, A62, Th38;
A64: 2 |^ (((N1 + N2) + 1) + 1) = 2 |^ ((N1 + 1) + (N2 + 1))
.= (2 |^ (N1 + 1)) * (2 |^ (N2 + 1)) by NEWTON:8 ;
(((((2 * i1) * i2) + i1) + i2) * 2) + 1 = ((2 * i1) + 1) * ((2 * i2) + 1) ;
then ((((((2 * i1) * i2) + i1) + i2) * 2) + 1) / (2 |^ (((N1 + N2) + 1) + 1)) = d1 * d2 by A17, A18, A64, XCMPLX_1:76;
hence (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) by A60, A63, SURREALO:4; :: thesis: verum

end;

end;

end;

end;

end;

A65: for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A5);
consider i1 being Integer, n1 being Nat such that
A66: d1 = i1 / (2 |^ n1) by Th18;
consider i2 being Integer, n2 being Nat such that
A67: d2 = i2 / (2 |^ n2) by Th18;
A68: ( d2 in DYADIC n2 & DYADIC n2 c= DYADIC (n1 + n2) ) by A67, Def4, Th19, NAT_1:11;
A69: d1 in DYADIC n1 by A66, Def4;
A70: n1 <= n1 + n2 by NAT_1:11;
S₁[n1 + (n1 + n2)] by A65;
hence (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2) by A68, A69, A70; :: thesis: verum