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) = [(((L_ (sReal . r1)) ++ {(sReal . r2)}) \/ ({(sReal . r1)} ++ (L_ (sReal . r2)))),(((R_ (sReal . r1)) ++ {(sReal . r2)}) \/ ({(sReal . r1)} ++ (R_ (sReal . r2))))] by SURREALR:28;
( (L_ (sReal . r1)) ++ {(sReal . r2)} << {(sReal . (r1 + r2))} & {(sReal . r1)} ++ (L_ (sReal . r2)) = (L_ (sReal . r2)) ++ {(sReal . r1)} & (L_ (sReal . r2)) ++ {(sReal . r1)} << {(sReal . (r1 + r2))} ) by Lm11;
then A2: L_ ((sReal . r1) + (sReal . r2)) << {(sReal . (r1 + r2))} by A1, SURREAL0:41;
{((sReal . r1) + (sReal . r2))} << R_ (sReal . (r1 + r2))

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in {((sReal . r1) + (sReal . r2))} or not b in R_ (sReal . (r1 + r2)) or not b <= a )
assume A3: ( a in {((sReal . r1) + (sReal . r2))} & b in R_ (sReal . (r1 + r2)) ) ; :: thesis: not b <= a
A4: a = (sReal . r1) + (sReal . r2) by A3, TARSKI:def 1;
consider n being Nat such that
A5: b = uDyadic . ([\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n)) by A3, Th43;
set d = [\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n);
set r = (([\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n)) - (r1 + r2)) / 2;
A6: 0 < ([\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n)) - (r1 + r2) by Th41, XREAL_1:50;
then consider n1 being Nat such that
A7: [\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1) < r1 + ((([\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n)) - (r1 + r2)) / 2) by Th53, XREAL_1:29;
consider n2 being Nat such that
A8: [\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2) < r2 + ((([\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n)) - (r1 + r2)) / 2) by A6, XREAL_1:29, Th53;
( sReal . r1 <= uDyadic . ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) & sReal . r2 < uDyadic . ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) ) by Th44;
then A9: (sReal . r1) + (sReal . r2) < (uDyadic . ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1))) + (uDyadic . ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2))) by SURREALR:44;
A10: (uDyadic . ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1))) + (uDyadic . ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2))) == uDyadic . (([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) + ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2))) by Th39;
(r1 + ((([\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n)) - (r1 + r2)) / 2)) + (r2 + ((([\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n)) - (r1 + r2)) / 2)) = [\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n) ;
then ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1)) + ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2)) < [\(((r1 + r2) * (2 |^ n)) + 1)/] / (2 |^ n) by A7, A8, XREAL_1:8;
then (uDyadic . ([\((r1 * (2 |^ n1)) + 1)/] / (2 |^ n1))) + (uDyadic . ([\((r2 * (2 |^ n2)) + 1)/] / (2 |^ n2))) <= b by SURREALO:4, A10, A5, Th24;
hence not b <= a by A4, SURREALO:4, A9; :: thesis: verum

end;

hence (sReal . r1) + (sReal . r2) <= sReal . (r1 + r2) by SURREAL0:43, A2; :: according to SURREALO:def 2 :: thesis: sReal . (r1 + r2) <= (sReal . r1) + (sReal . r2)
A11: 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 A12: ( a in L_ (sReal . (r1 + r2)) & b in {((sReal . r1) + (sReal . r2))} ) ; :: thesis: not b <= a
A13: b = (sReal . r1) + (sReal . r2) by A12, TARSKI:def 1;
consider n being Nat such that
A14: a = uDyadic . ([/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n)) by A12, Th42;
set d = [/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n);
set r = ((r1 + r2) - ([/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n))) / 2;
A15: 0 < (r1 + r2) - ([/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n)) by Th41, XREAL_1:50;
then consider n1 being Nat such that
A16: r1 - (((r1 + r2) - ([/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n))) / 2) < [/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1) by XREAL_1:44, Th54;
consider n2 being Nat such that
A17: r2 - (((r1 + r2) - ([/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n))) / 2) < [/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2) by A15, XREAL_1:44, Th54;
( uDyadic . ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) <= sReal . r1 & uDyadic . ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) < sReal . r2 ) by Th44;
then A18: (uDyadic . ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1))) + (uDyadic . ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2))) < (sReal . r1) + (sReal . r2) by SURREALR:44;
A19: (uDyadic . ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1))) + (uDyadic . ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2))) == uDyadic . (([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) + ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2))) by Th39;
(r1 - (((r1 + r2) - ([/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n))) / 2)) + (r2 - (((r1 + r2) - ([/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n))) / 2)) = [/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n) ;
then [/(((r1 + r2) * (2 |^ n)) - 1)\] / (2 |^ n) < ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1)) + ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2)) by A16, A17, XREAL_1:8;
then a <= (uDyadic . ([/((r1 * (2 |^ n1)) - 1)\] / (2 |^ n1))) + (uDyadic . ([/((r2 * (2 |^ n2)) - 1)\] / (2 |^ n2))) by A14, Th24, SURREALO:4, A19;
hence not b <= a by A13, SURREALO:4, A18; :: thesis: verum

end;

( {(sReal . (r1 + r2))} << (R_ (sReal . r1)) ++ {(sReal . r2)} & {(sReal . (r1 + r2))} << {(sReal . r1)} ++ (R_ (sReal . r2)) ) by Lm12;
then {(sReal . (r1 + r2))} << R_ ((sReal . r1) + (sReal . r2)) by A1, SURREAL0:42;
hence sReal . (r1 + r2) <= (sReal . r1) + (sReal . r2) by A11, SURREAL0:43; :: thesis: verum