let r1, r2 be Real; :: thesis: (sReal . r1) * (sReal . r2) == sReal . (r1 * r2)
set r12 = r1 * r2;
set R1 = sReal . r1;
set R2 = sReal . r2;
set R12 = sReal . (r1 * r2);
A1: (sReal . r1) * (sReal . r2) = [((comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2)))) \/ (comp ((R_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2))))),((comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2)))) \/ (comp ((R_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2)))))] by SURREALR:50;
A2: comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2))) << {(sReal . (r1 * r2))}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2))) or not b in {(sReal . (r1 * r2))} or not b <= a )
assume A3: ( a in comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2))) & b in {(sReal . (r1 * r2))} ) ; :: thesis: not b <= a
consider x1, y1 being Surreal such that
A4: ( a = ((x1 * (sReal . r2)) + ((sReal . r1) * y1)) - (x1 * y1) & x1 in L_ (sReal . r1) & y1 in L_ (sReal . r2) ) by A3, SURREALR:def 15;
consider n1 being Nat such that
A5: x1 = uDyadic . ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) by Th42, A4;
set d1 = [/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1);
consider n2 being Nat such that
A6: y1 = uDyadic . ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) by Th42, A4;
set d2 = [/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2);
A7: a == sReal . (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (r1 * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) by A4, A5, A6, Lm18;
( 0 < r1 - ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) & 0 < r2 - ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) ) by Th41, XREAL_1:50;
then 0 < (r1 - ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1))) * (r2 - ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2))) ;
then 0 < (r1 * r2) - (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) * r1)) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) ;
then consider k being Nat such that
A8: ((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) * r1)) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2))) < [/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k) by Th54, XREAL_1:47;
set d = [/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k);
( sReal . (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (r1 * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) < sReal . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) & sReal . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) == uDyadic . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) ) by A8, Th50, Th46;
then ( sReal . (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (r1 * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) <= uDyadic . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) & uDyadic . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) < sReal . (r1 * r2) ) by Th44, SURREALO:4;
then ( sReal . (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (r1 * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) < sReal . (r1 * r2) & sReal . (r1 * r2) = b ) by SURREALO:4, A3, TARSKI:def 1;
hence not b <= a by A7, SURREALO:4; :: thesis: verum

end;

comp ((R_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2))) << {(sReal . (r1 * r2))}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in comp ((R_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2))) or not b in {(sReal . (r1 * r2))} or not b <= a )
assume A9: ( a in comp ((R_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2))) & b in {(sReal . (r1 * r2))} ) ; :: thesis: not b <= a
consider x1, y1 being Surreal such that
A10: ( a = ((x1 * (sReal . r2)) + ((sReal . r1) * y1)) - (x1 * y1) & x1 in R_ (sReal . r1) & y1 in R_ (sReal . r2) ) by A9, SURREALR:def 15;
consider n1 being Nat such that
A11: x1 = uDyadic . ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) by Th43, A10;
set d1 = [\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1);
consider n2 being Nat such that
A12: y1 = uDyadic . ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) by Th43, A10;
set d2 = [\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2);
A13: a == sReal . (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (r1 * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) by A10, A11, A12, Lm18;
( r1 - ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) < 0 & r2 - ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) < 0 ) by Th41, XREAL_1:49;
then 0 < (r1 - ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1))) * (r2 - ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2))) ;
then 0 < (r1 * r2) - (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) * r1)) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) ;
then consider k being Nat such that
A14: ((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) * r1)) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2))) < [/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k) by Th54, XREAL_1:47;
set d = [/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k);
( sReal . (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (r1 * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) < sReal . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) & sReal . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) == uDyadic . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) ) by A14, Th50, Th46;
then ( sReal . (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (r1 * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) <= uDyadic . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) & uDyadic . ([/(((r1 * r2) * (2 |^ k)) - 1)\] / (2 |^ k)) < sReal . (r1 * r2) ) by Th44, SURREALO:4;
then ( sReal . (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (r1 * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) < sReal . (r1 * r2) & sReal . (r1 * r2) = b ) by SURREALO:4, A9, TARSKI:def 1;
hence not b <= a by A13, SURREALO:4; :: thesis: verum

end;

then A15: L_ ((sReal . r1) * (sReal . r2)) << {(sReal . (r1 * r2))} by A1, A2, SURREAL0:41;
A16: {(sReal . (r1 * r2))} << comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2)))

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not b in {(sReal . (r1 * r2))} or not a in comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2))) or not a <= b )
assume A17: ( b in {(sReal . (r1 * r2))} & a in comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2))) ) ; :: thesis: not a <= b
consider x1, y1 being Surreal such that
A18: ( a = ((x1 * (sReal . r2)) + ((sReal . r1) * y1)) - (x1 * y1) & x1 in L_ (sReal . r1) & y1 in R_ (sReal . r2) ) by A17, SURREALR:def 15;
consider n1 being Nat such that
A19: x1 = uDyadic . ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) by Th42, A18;
set d1 = [/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1);
consider n2 being Nat such that
A20: y1 = uDyadic . ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) by Th43, A18;
set d2 = [\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2);
A21: a == sReal . (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (r1 * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) by A18, A19, A20, Lm18;
( 0 < r1 - ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) & r2 - ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) < 0 ) by Th41, XREAL_1:49, XREAL_1:50;
then (r1 - ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1))) * (r2 - ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2))) < 0 ;
then (r1 * r2) - (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) * r1)) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) < 0 ;
then consider k being Nat such that
A22: [\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k) < ((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) * r1)) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2))) by Th53, XREAL_1:48;
set d = [\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k);
( uDyadic . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) == sReal . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) & sReal . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) < sReal . (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (r1 * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) ) by A22, Th50, Th46;
then ( sReal . (r1 * r2) < uDyadic . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) & uDyadic . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) <= sReal . (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (r1 * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) ) by Th44, SURREALO:4;
then ( b = sReal . (r1 * r2) & sReal . (r1 * r2) < sReal . (((([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * r2) + (r1 * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) - (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) * ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)))) ) by SURREALO:4, A17, TARSKI:def 1;
hence not a <= b by A21, SURREALO:4; :: thesis: verum

end;

{(sReal . (r1 * r2))} << comp ((R_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2)))

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not b in {(sReal . (r1 * r2))} or not a in comp ((R_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2))) or not a <= b )
assume A23: ( b in {(sReal . (r1 * r2))} & a in comp ((R_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2))) ) ; :: thesis: not a <= b
consider x1, y1 being Surreal such that
A24: ( a = ((x1 * (sReal . r2)) + ((sReal . r1) * y1)) - (x1 * y1) & x1 in R_ (sReal . r1) & y1 in L_ (sReal . r2) ) by A23, SURREALR:def 15;
consider n1 being Nat such that
A25: x1 = uDyadic . ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) by Th43, A24;
set d1 = [\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1);
consider n2 being Nat such that
A26: y1 = uDyadic . ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) by Th42, A24;
set d2 = [/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2);
A27: a == sReal . (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (r1 * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) by A24, A25, A26, Lm18;
( 0 < r2 - ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) & r1 - ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) < 0 ) by Th41, XREAL_1:49, XREAL_1:50;
then (r1 - ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1))) * (r2 - ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2))) < 0 ;
then (r1 * r2) - (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) * r1)) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) < 0 ;
then consider k being Nat such that
A28: [\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k) < ((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) * r1)) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2))) by Th53, XREAL_1:48;
set d = [\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k);
( uDyadic . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) == sReal . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) & sReal . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) < sReal . (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (r1 * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) ) by A28, Th50, Th46;
then ( sReal . (r1 * r2) < uDyadic . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) & uDyadic . ([\(((r1 * r2) * (2 |^ k)) + 1)/] / (2 |^ k)) <= sReal . (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (r1 * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) ) by Th44, SURREALO:4;
then ( b = sReal . (r1 * r2) & sReal . (r1 * r2) < sReal . (((([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * r2) + (r1 * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) - (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) * ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)))) ) by SURREALO:4, A23, TARSKI:def 1;
hence not a <= b by A27, SURREALO:4; :: thesis: verum

end;

then A29: {(sReal . (r1 * r2))} << R_ ((sReal . r1) * (sReal . r2)) by A1, A16, SURREAL0:42;
A30: L_ (sReal . (r1 * r2)) << {((sReal . r1) * (sReal . r2))}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ (sReal . (r1 * r2)) or not b in {((sReal . r1) * (sReal . r2))} or not b <= a )
assume A31: ( a in L_ (sReal . (r1 * r2)) & b in {((sReal . r1) * (sReal . r2))} ) ; :: thesis: not b <= a
consider n being Nat such that
A32: a = uDyadic . ([/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n)) by Th42, A31;
set d = [/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n);
0 < (r1 * r2) - ([/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n)) by Th41, XREAL_1:50;
then consider k being Nat such that
A33: 1 / (2 |^ k) <= (r1 * r2) - ([/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n)) by PREPOWER:92;
set M = 1 / (2 |^ k);
consider k1 being Nat such that
A34: r1 - (1 / (2 |^ k)) < [/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1) by Th54, XREAL_1:44;
set d1 = [/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1);
consider k2 being Nat such that
A35: r2 - (1 / (2 |^ k)) < [/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2) by Th54, XREAL_1:44;
set d2 = [/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2);
( 0 < r1 - ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) & r1 - ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) < 1 / (2 |^ k) & 0 < r2 - ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)) & r2 - ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)) < 1 / (2 |^ k) ) by Th41, A34, A35, XREAL_1:11, XREAL_1:50;
then ( 0 < (r1 - ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (r2 - ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) & (r1 - ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (r2 - ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) < (1 / (2 |^ k)) * (1 / (2 |^ k)) ) by XREAL_1:96;
then (r1 * r2) - (((r1 * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) < (1 / (2 |^ k)) * (1 / (2 |^ k)) ;
then A36: (r1 * r2) - ((1 / (2 |^ k)) * (1 / (2 |^ k))) < ((r1 * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) by XREAL_1:11;
1 <= 1 * (2 |^ k) by NAT_1:14;
then 1 / (2 |^ k) <= 1 by XREAL_1:79;
then A37: (1 / (2 |^ k)) * (1 / (2 |^ k)) <= (1 / (2 |^ k)) * 1 by XREAL_1:64;
( [/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n) <= (r1 * r2) - (1 / (2 |^ k)) & (r1 * r2) - (1 / (2 |^ k)) <= (r1 * r2) - ((1 / (2 |^ k)) * (1 / (2 |^ k))) ) by A33, A37, XREAL_1:10, XREAL_1:11;
then [/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n) <= (r1 * r2) - ((1 / (2 |^ k)) * (1 / (2 |^ k))) by XXREAL_0:2;
then [/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n) < ((r1 * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) by A36, XXREAL_0:2;
then ( a == sReal . ([/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n)) & sReal . ([/(((r1 * r2) * (2 |^ n)) - 1)\] / (2 |^ n)) < sReal . (((r1 * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) ) by A32, Th50, Th46;
then A38: a <= sReal . (((r1 * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) by SURREALO:4;
A39: ( L_ ((sReal . r1) * (sReal . r2)) << {((sReal . r1) * (sReal . r2))} & (sReal . r1) * (sReal . r2) in {((sReal . r1) * (sReal . r2))} ) by TARSKI:def 1, SURREALO:11;
( uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) in L_ (sReal . r1) & uDyadic . ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)) in L_ (sReal . r2) ) by Th42;
then (((sReal . r1) * (uDyadic . ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) + ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (sReal . r2))) - ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (uDyadic . ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) in comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(L_ (sReal . r2))) by SURREALR:def 15;
then A40: (((sReal . r1) * (uDyadic . ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) + ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (sReal . r2))) + (- ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (uDyadic . ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))))) in L_ ((sReal . r1) * (sReal . r2)) by XBOOLE_0:def 3, A1;
(((sReal . r1) * (uDyadic . ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) + ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (sReal . r2))) + (- ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (uDyadic . ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))))) == sReal . (((r1 * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) by Lm18;
then sReal . (((r1 * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([/((r2 * (2 |^ k2)) - 1)\] / (2 |^ k2)))) < (sReal . r1) * (sReal . r2) by A40, A39, SURREALO:4;
then a < (sReal . r1) * (sReal . r2) by A38, SURREALO:4;
hence not b <= a by A31, TARSKI:def 1; :: thesis: verum

end;

{((sReal . r1) * (sReal . r2))} << R_ (sReal . (r1 * r2))

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not b in {((sReal . r1) * (sReal . r2))} or not a in R_ (sReal . (r1 * r2)) or not a <= b )
assume A41: ( b in {((sReal . r1) * (sReal . r2))} & a in R_ (sReal . (r1 * r2)) ) ; :: thesis: not a <= b
consider n being Nat such that
A42: a = uDyadic . ([\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n)) by Th43, A41;
set d = [\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n);
0 < ([\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n)) - (r1 * r2) by Th41, XREAL_1:50;
then consider k being Nat such that
A43: 1 / (2 |^ k) <= ([\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n)) - (r1 * r2) by PREPOWER:92;
set M = 1 / (2 |^ k);
consider k1 being Nat such that
A44: r1 - (1 / (2 |^ k)) < [/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1) by Th54, XREAL_1:44;
set d1 = [/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1);
consider k2 being Nat such that
A45: [\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2) < r2 + (1 / (2 |^ k)) by Th53, XREAL_1:29;
set d2 = [\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2);
( 0 < r1 - ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) & r1 - ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) < 1 / (2 |^ k) & 0 < ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)) - r2 & ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)) - r2 < 1 / (2 |^ k) ) by Th41, A44, A45, XREAL_1:11, XREAL_1:19, XREAL_1:50;
then ( 0 < (r1 - ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)) - r2) & (r1 - ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)) - r2) < (1 / (2 |^ k)) * (1 / (2 |^ k)) ) by XREAL_1:96;
then (((r1 * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) - (r1 * r2) < (1 / (2 |^ k)) * (1 / (2 |^ k)) ;
then A46: ((r1 * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) < ((1 / (2 |^ k)) * (1 / (2 |^ k))) + (r1 * r2) by XREAL_1:19;
1 <= 1 * (2 |^ k) by NAT_1:14;
then 1 / (2 |^ k) <= 1 by XREAL_1:79;
then A47: (1 / (2 |^ k)) * (1 / (2 |^ k)) <= (1 / (2 |^ k)) * 1 by XREAL_1:64;
( [\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n) >= (r1 * r2) + (1 / (2 |^ k)) & (r1 * r2) + (1 / (2 |^ k)) >= (r1 * r2) + ((1 / (2 |^ k)) * (1 / (2 |^ k))) ) by A43, A47, XREAL_1:6, XREAL_1:19;
then [\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n) >= (r1 * r2) + ((1 / (2 |^ k)) * (1 / (2 |^ k))) by XXREAL_0:2;
then [\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n) > ((r1 * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) by A46, XXREAL_0:2;
then ( sReal . (((r1 * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) < sReal . ([\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n)) & sReal . ([\(((r1 * r2) * (2 |^ n)) + 1)/] / (2 |^ n)) == a ) by A42, Th50, Th46;
then A48: sReal . (((r1 * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) <= a by SURREALO:4;
A49: ( {((sReal . r1) * (sReal . r2))} << R_ ((sReal . r1) * (sReal . r2)) & (sReal . r1) * (sReal . r2) in {((sReal . r1) * (sReal . r2))} ) by TARSKI:def 1, SURREALO:11;
( uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) in L_ (sReal . r1) & uDyadic . ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)) in R_ (sReal . r2) ) by Th42, Th43;
then (((sReal . r1) * (uDyadic . ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) + ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (sReal . r2))) - ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (uDyadic . ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) in comp ((L_ (sReal . r1)),(sReal . r1),(sReal . r2),(R_ (sReal . r2))) by SURREALR:def 15;
then A50: (((sReal . r1) * (uDyadic . ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) + ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (sReal . r2))) + (- ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (uDyadic . ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))))) in R_ ((sReal . r1) * (sReal . r2)) by XBOOLE_0:def 3, A1;
(((sReal . r1) * (uDyadic . ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) + ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (sReal . r2))) + (- ((uDyadic . ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1))) * (uDyadic . ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))))) == sReal . (((r1 * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) by Lm18;
then (sReal . r1) * (sReal . r2) < sReal . (((r1 * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2))) + (r2 * ([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)))) - (([/((r1 * (2 |^ k1)) - 1)\] / (2 |^ k1)) * ([\((r2 * (2 |^ k2)) + 1)/] / (2 |^ k2)))) by A50, A49, SURREALO:4;
then (sReal . r1) * (sReal . r2) < a by A48, SURREALO:4;
hence not a <= b by A41, TARSKI:def 1; :: thesis: verum

end;

hence (sReal . r1) * (sReal . r2) == sReal . (r1 * r2) by A15, A29, A30, SURREAL0:43; :: thesis: verum