let A be Ordinal; :: thesis: for y being positive decreasing_infinitely Surreal-Sequence
for r, s being Sequence of REAL st dom r = dom s & A c= (dom r) /\ (dom y) holds
Sum (((r + s) | A),(y | A)) == (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A)))
let y be positive decreasing_infinitely Surreal-Sequence; :: thesis: for r, s being Sequence of REAL st dom r = dom s & A c= (dom r) /\ (dom y) holds
Sum (((r + s) | A),(y | A)) == (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A)))
defpred S₁[ Ordinal] means for r, s being Sequence of REAL st dom r = dom s & $1 c= (dom r) /\ (dom y) holds
Sum (((r + s) | $1),(y | $1)) == (Sum ((r | $1),(y | $1))) + (Sum ((s | $1),(y | $1)));
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
S₁[C] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S₁[C] ) implies S₁[A] )
assume A2: for C being Ordinal st C in A holds
S₁[C] ; :: thesis: S₁[A]
A3: for r, s being Sequence of REAL st dom r = dom s holds
for B being Ordinal
for e being positive Real st B in A & A c= (dom r) /\ (dom y) holds
( Sum (((r + s) | A),(y | A)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) & (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) < Sum (((r + s) | A),(y | A)) )

proof

let r, s be Sequence of REAL ; :: thesis: ( dom r = dom s implies for B being Ordinal
for e being positive Real st B in A & A c= (dom r) /\ (dom y) holds
( Sum (((r + s) | A),(y | A)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) & (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) < Sum (((r + s) | A),(y | A)) ) )
assume A4: dom r = dom s ; :: thesis: for B being Ordinal
for e being positive Real st B in A & A c= (dom r) /\ (dom y) holds
( Sum (((r + s) | A),(y | A)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) & (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) < Sum (((r + s) | A),(y | A)) )
let B be Ordinal; :: thesis: for e being positive Real st B in A & A c= (dom r) /\ (dom y) holds
( Sum (((r + s) | A),(y | A)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) & (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) < Sum (((r + s) | A),(y | A)) )
let e be positive Real; :: thesis: ( B in A & A c= (dom r) /\ (dom y) implies ( Sum (((r + s) | A),(y | A)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) & (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) < Sum (((r + s) | A),(y | A)) ) )
assume A5: ( B in A & A c= (dom r) /\ (dom y) ) ; :: thesis: ( Sum (((r + s) | A),(y | A)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) & (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) < Sum (((r + s) | A),(y | A)) )
set rs = r + s;
A6: dom (r + s) = (dom r) /\ (dom s) by VALUED_1:def 1;
reconsider Srs = [ { ((Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) - e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) + e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } ] as Surreal by A4, A5, A6, Th61;
reconsider Sr = [ { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } ] as Surreal by A5, Th61;
( Unique_No Srs = Sum (((r + s) | A),(y | A)) & Unique_No Sr = Sum ((r | A),(y | A)) ) by A4, A5, A6, Th62;
then A7: ( Srs == Sum (((r + s) | A),(y | A)) & Sr == Sum ((r | A),(y | A)) ) by SURREALO:def 10;
A8: Sum (((r + s) | B),(y | B)) == (Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B))) by A2, A4, A5, ORDINAL1:def 2;
set e2 = e / 2;
B in dom (r + s) by A4, A5, A6, XBOOLE_0:def 4;
then (r . B) + (s . B) = (r + s) . B by VALUED_1:def 1;
then A9: ( ((r . B) - (e / 2)) + ((s . B) + e) = ((r + s) . B) + (e / 2) & ((r . B) + (e / 2)) + ((s . B) - e) = ((r + s) . B) - (e / 2) ) ;
( ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + (Sum ((s | B),(y | B))) < (Sum ((r | A),(y | A))) + (Sum ((s | B),(y | B))) & (Sum ((r | A),(y | A))) + (Sum ((s | B),(y | B))) < ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + (Sum ((s | B),(y | B))) ) by SURREALR:44, Th69, A5;
then ( (Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B)) <= ((Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B)))) + ((uReal . ((r . B) - (e / 2))) * (y .. B)) & ((Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B)))) + ((uReal . ((r . B) - (e / 2))) * (y .. B)) < (Sum ((r | A),(y | A))) + (Sum ((s | B),(y | B))) & (Sum ((r | A),(y | A))) + (Sum ((s | B),(y | B))) < ((Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B)))) + ((uReal . ((r . B) + (e / 2))) * (y .. B)) & ((Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B)))) + ((uReal . ((r . B) + (e / 2))) * (y .. B)) <= (Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B)) ) by A8, SURREALR:32, SURREALR:37;
then A10: ( (Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B)) < (Sum ((r | A),(y | A))) + (Sum ((s | B),(y | B))) & (Sum ((r | A),(y | A))) + (Sum ((s | B),(y | B))) < (Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B)) ) by SURREALO:9;
then ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + ((uReal . ((s . B) + e)) * (y .. B)) < ((Sum ((r | A),(y | A))) + (Sum ((s | B),(y | B)))) + ((uReal . ((s . B) + e)) * (y .. B)) by SURREALR:32;
then ( (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) + (e / 2))) * (y .. B)) == ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + ((uReal . ((s . B) + e)) * (y .. B)) & ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + ((uReal . ((s . B) + e)) * (y .. B)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) ) by A9, SURREALR:37, Th30;
then A11: (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) + (e / 2))) * (y .. B)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) by SURREALO:9;
((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + ((uReal . ((s . B) - e)) * (y .. B)) > ((Sum ((r | A),(y | A))) + (Sum ((s | B),(y | B)))) + ((uReal . ((s . B) - e)) * (y .. B)) by A10, SURREALR:32;
then ( (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) - (e / 2))) * (y .. B)) == ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + ((uReal . ((s . B) - e)) * (y .. B)) & ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + ((uReal . ((s . B) - e)) * (y .. B)) > (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) ) by SURREALR:37, A9, Th30;
then A12: (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) - (e / 2))) * (y .. B)) > (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) by SURREALO:9;
A13: ( (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) + (e / 2))) * (y .. B)) in R_ Srs & Srs in {Srs} & {Srs} << R_ Srs ) by TARSKI:def 1, A5, SURREALO:11;
then (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) + (e / 2))) * (y .. B)) > Sum (((r + s) | A),(y | A)) by A7, SURREALO:9;
then (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) + (e / 2))) * (y .. B)) >= Sum (((r + s) | A),(y | A)) by SURREALO:6;
hence Sum (((r + s) | A),(y | A)) < (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) by A11, SURREALO:4; :: thesis: (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) < Sum (((r + s) | A),(y | A))
( (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) - (e / 2))) * (y .. B)) in L_ Srs & L_ Srs << {Srs} ) by A5, SURREALO:11;
then (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) - (e / 2))) * (y .. B)) <= Sum (((r + s) | A),(y | A)) by A7, A13, SURREALO:9;
hence Sum (((r + s) | A),(y | A)) > (Sum ((r | A),(y | A))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) by A12, SURREALO:4; :: thesis: verum

end;

let r, s be Sequence of REAL ; :: thesis: ( dom r = dom s & A c= (dom r) /\ (dom y) implies Sum (((r + s) | A),(y | A)) == (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) )
assume A14: ( dom r = dom s & A c= (dom r) /\ (dom y) ) ; :: thesis: Sum (((r + s) | A),(y | A)) == (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A)))
set rs = r + s;
A15: dom (r + s) = (dom r) /\ (dom s) by VALUED_1:def 1;
reconsider Sr = [ { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } ] as Surreal by A14, Th61;
reconsider Ss = [ { ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } ] as Surreal by A14, Th61;
reconsider Srs = [ { ((Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) - e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) + e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } ] as Surreal by A14, A15, Th61;
( Unique_No Sr = Sum ((r | A),(y | A)) & Unique_No Ss = Sum ((s | A),(y | A)) & Unique_No Srs = Sum (((r + s) | A),(y | A)) ) by A14, A15, Th62;
then A16: ( Sr == Sum ((r | A),(y | A)) & Ss == Sum ((s | A),(y | A)) & Srs == Sum (((r + s) | A),(y | A)) ) by SURREALO:def 10;
A17: Sr + Ss = [(((L_ Sr) ++ {Ss}) \/ ({Sr} ++ (L_ Ss))),(((R_ Sr) ++ {Ss}) \/ ({Sr} ++ (R_ Ss)))] by SURREALR:28;
A18: L_ (Sr + Ss) << {Srs}

proof

let x, yy be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in L_ (Sr + Ss) or not yy in {Srs} or not yy <= x )
assume A19: ( x in L_ (Sr + Ss) & yy in {Srs} ) ; :: thesis: not yy <= x

per cases ( x in (L_ Sr) ++ {Ss} or x in {Sr} ++ (L_ Ss) ) by A17, A19, XBOOLE_0:def 3;

suppose x in (L_ Sr) ++ {Ss} ; :: thesis: not yy <= x

then consider a, b being Surreal such that
A20: ( a in L_ Sr & b in {Ss} & a + b = x ) by SURREALR:def 8;
consider B being Element of A, e being positive Real such that
A21: ( a = (Sum ((r | B),(y | B))) + ((uReal . ((r . B) - e)) * (y .. B)) & B in A ) by A20;
A22: ( Ss + a == (Sum ((s | A),(y | A))) + a & (Sum ((s | A),(y | A))) + a < Srs ) by A16, A21, A14, A3, SURREALO:4, SURREALR:43;
( b = Ss & yy = Srs ) by A19, A20, TARSKI:def 1;
hence not yy <= x by A20, A22, SURREALO:4; :: thesis: verum

end;

suppose x in {Sr} ++ (L_ Ss) ; :: thesis: not yy <= x

then consider a, b being Surreal such that
A23: ( a in {Sr} & b in L_ Ss & a + b = x ) by SURREALR:def 8;
consider B being Element of A, e being positive Real such that
A24: ( b = (Sum ((s | B),(y | B))) + ((uReal . ((s . B) - e)) * (y .. B)) & B in A ) by A23;
A25: ( Sr + b == (Sum ((r | A),(y | A))) + b & (Sum ((r | A),(y | A))) + b < Srs ) by A14, A24, A3, A16, SURREALO:4, SURREALR:43;
( a = Sr & yy = Srs ) by A19, A23, TARSKI:def 1;
hence not yy <= x by A23, A25, SURREALO:4; :: thesis: verum

end;

end;

end;

{(Sr + Ss)} << R_ Srs

proof

let x, yy be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in {(Sr + Ss)} or not yy in R_ Srs or not yy <= x )
assume A26: ( x in {(Sr + Ss)} & yy in R_ Srs ) ; :: thesis: not yy <= x
consider B being Element of A, e being positive Real such that
A27: ( yy = (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) + e)) * (y .. B)) & B in A ) by A26;
set e2 = e / 2;
( Sum ((r | A),(y | A)) < (Sum ((r | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B)) & Sum ((s | A),(y | A)) <= (Sum ((s | B),(y | B))) + ((uReal . ((s . B) + (e / 2))) * (y .. B)) ) by Th69, A14, A27;
then A28: (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) < ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) by SURREALR:44;
(Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) == Sr + Ss by A16, SURREALR:43;
then A29: (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) == x by A26, TARSKI:def 1;
A30: ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) = (Sum ((r | B),(y | B))) + (((uReal . ((r . B) + (e / 2))) * (y .. B)) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + (e / 2))) * (y .. B)))) by SURREALR:37
.= (Sum ((r | B),(y | B))) + ((((uReal . ((r . B) + (e / 2))) * (y .. B)) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) + (Sum ((s | B),(y | B)))) by SURREALR:37
.= ((Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B)))) + (((uReal . ((r . B) + (e / 2))) * (y .. B)) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) by SURREALR:37 ;
B in dom (r + s) by A14, A15, A27, XBOOLE_0:def 4;
then (r . B) + (s . B) = (r + s) . B by VALUED_1:def 1;
then A31: ((r . B) + (e / 2)) + ((s . B) + (e / 2)) = ((r + s) . B) + e ;
Sum (((r + s) | B),(y | B)) == (Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B))) by A2, A27, A14, ORDINAL1:def 2;
then ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) <= (Sum (((r + s) | B),(y | B))) + (((uReal . ((r . B) + (e / 2))) * (y .. B)) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) by A30, SURREALR:43;
then (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) < (Sum (((r + s) | B),(y | B))) + (((uReal . ((r . B) + (e / 2))) * (y .. B)) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) by A28, SURREALO:4;
then ( x < (Sum (((r + s) | B),(y | B))) + (((uReal . ((r . B) + (e / 2))) * (y .. B)) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) & (Sum (((r + s) | B),(y | B))) + (((uReal . ((r . B) + (e / 2))) * (y .. B)) + ((uReal . ((s . B) + (e / 2))) * (y .. B))) = ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + ((uReal . ((s . B) + (e / 2))) * (y .. B)) & ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) + (e / 2))) * (y .. B))) + ((uReal . ((s . B) + (e / 2))) * (y .. B)) == yy ) by A31, Th30, A29, SURREALO:4, SURREALR:37, A27;
hence not yy <= x by SURREALO:4; :: thesis: verum

end;

then A32: Sr + Ss <= Srs by A18, SURREAL0:43;
A33: {Srs} << R_ (Sr + Ss)

proof

let yy, x be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not yy in {Srs} or not x in R_ (Sr + Ss) or not x <= yy )
assume A34: ( yy in {Srs} & x in R_ (Sr + Ss) ) ; :: thesis: not x <= yy

per cases ( x in (R_ Sr) ++ {Ss} or x in {Sr} ++ (R_ Ss) ) by A17, A34, XBOOLE_0:def 3;

suppose x in (R_ Sr) ++ {Ss} ; :: thesis: not x <= yy

then consider a, b being Surreal such that
A35: ( a in R_ Sr & b in {Ss} & a + b = x ) by SURREALR:def 8;
consider B being Element of A, e being positive Real such that
A36: ( a = (Sum ((r | B),(y | B))) + ((uReal . ((r . B) + e)) * (y .. B)) & B in A ) by A35;
A37: ( Ss + a == (Sum ((s | A),(y | A))) + a & (Sum ((s | A),(y | A))) + a > Srs ) by A16, A36, A14, A3, SURREALO:4, SURREALR:43;
( b = Ss & yy = Srs ) by A34, A35, TARSKI:def 1;
hence not x <= yy by A35, A37, SURREALO:4; :: thesis: verum

end;

suppose x in {Sr} ++ (R_ Ss) ; :: thesis: not x <= yy

then consider a, b being Surreal such that
A38: ( a in {Sr} & b in R_ Ss & a + b = x ) by SURREALR:def 8;
consider B being Element of A, e being positive Real such that
A39: ( b = (Sum ((s | B),(y | B))) + ((uReal . ((s . B) + e)) * (y .. B)) & B in A ) by A38;
A40: ( Sr + b == (Sum ((r | A),(y | A))) + b & (Sum ((r | A),(y | A))) + b > Srs ) by A14, A39, A3, A16, SURREALO:4, SURREALR:43;
( a = Sr & yy = Srs ) by A34, A38, TARSKI:def 1;
hence not x <= yy by A38, A40, SURREALO:4; :: thesis: verum

end;

end;

end;

L_ Srs << {(Sr + Ss)}

proof

let yy, x be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not yy in L_ Srs or not x in {(Sr + Ss)} or not x <= yy )
assume A41: ( yy in L_ Srs & x in {(Sr + Ss)} ) ; :: thesis: not x <= yy
consider B being Element of A, e being positive Real such that
A42: ( yy = (Sum (((r + s) | B),(y | B))) + ((uReal . (((r + s) . B) - e)) * (y .. B)) & B in A ) by A41;
set e2 = e / 2;
( Sum ((r | A),(y | A)) > (Sum ((r | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B)) & Sum ((s | A),(y | A)) > (Sum ((s | B),(y | B))) + ((uReal . ((s . B) - (e / 2))) * (y .. B)) ) by Th69, A14, A42;
then ( Sum ((r | A),(y | A)) > (Sum ((r | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B)) & Sum ((s | A),(y | A)) >= (Sum ((s | B),(y | B))) + ((uReal . ((s . B) - (e / 2))) * (y .. B)) ) by SURREALO:6;
then A43: (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) > ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) by SURREALR:44;
(Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) == Sr + Ss by A16, SURREALR:43;
then A44: (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) == x by A41, TARSKI:def 1;
A45: ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) = (Sum ((r | B),(y | B))) + (((uReal . ((r . B) - (e / 2))) * (y .. B)) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - (e / 2))) * (y .. B)))) by SURREALR:37
.= (Sum ((r | B),(y | B))) + ((((uReal . ((r . B) - (e / 2))) * (y .. B)) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) + (Sum ((s | B),(y | B)))) by SURREALR:37
.= ((Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B)))) + (((uReal . ((r . B) - (e / 2))) * (y .. B)) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) by SURREALR:37 ;
B in dom (r + s) by A14, A15, A42, XBOOLE_0:def 4;
then (r . B) + (s . B) = (r + s) . B by VALUED_1:def 1;
then A46: ((r . B) - (e / 2)) + ((s . B) - (e / 2)) = ((r + s) . B) - e ;
Sum (((r + s) | B),(y | B)) == (Sum ((r | B),(y | B))) + (Sum ((s | B),(y | B))) by A2, A42, A14, ORDINAL1:def 2;
then ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + ((Sum ((s | B),(y | B))) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) >= (Sum (((r + s) | B),(y | B))) + (((uReal . ((r . B) - (e / 2))) * (y .. B)) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) by A45, SURREALR:43;
then (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) > (Sum (((r + s) | B),(y | B))) + (((uReal . ((r . B) - (e / 2))) * (y .. B)) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) by A43, SURREALO:4;
then ( x > (Sum (((r + s) | B),(y | B))) + (((uReal . ((r . B) - (e / 2))) * (y .. B)) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) & (Sum (((r + s) | B),(y | B))) + (((uReal . ((r . B) - (e / 2))) * (y .. B)) + ((uReal . ((s . B) - (e / 2))) * (y .. B))) = ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + ((uReal . ((s . B) - (e / 2))) * (y .. B)) & ((Sum (((r + s) | B),(y | B))) + ((uReal . ((r . B) - (e / 2))) * (y .. B))) + ((uReal . ((s . B) - (e / 2))) * (y .. B)) == yy ) by A46, Th30, A44, SURREALO:4, SURREALR:37, A42;
hence not x <= yy by SURREALO:4; :: thesis: verum

end;

then A47: Sr + Ss >= Srs by A33, SURREAL0:43;
(Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) == Sr + Ss by A16, SURREALR:43;
then (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) == Srs by A32, A47, SURREALO:4;
hence Sum (((r + s) | A),(y | A)) == (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) by A16, SURREALO:4; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A1);
hence for r, s being Sequence of REAL st dom r = dom s & A c= (dom r) /\ (dom y) holds
Sum (((r + s) | A),(y | A)) == (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A))) ; :: thesis: verum