let A be Ordinal; :: thesis: for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T & dom y c= dom r & A c= dom y holds
(Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) = Sum (y,z,yz,r,s,S,T)
let r, s be Sequence of REAL ; :: thesis: for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T & dom y c= dom r & A c= dom y holds
(Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) = Sum (y,z,yz,r,s,S,T)
let y, z, yz be strictly_decreasing Surreal-Sequence; :: thesis: for S, T being non empty Ordinal st dom y c= S & dom z c= T & dom y c= dom r & A c= dom y holds
(Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) = Sum (y,z,yz,r,s,S,T)
let S, T be non empty Ordinal; :: thesis: ( dom y c= S & dom z c= T & dom y c= dom r & A c= dom y implies (Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) = Sum (y,z,yz,r,s,S,T) )
assume that
A1: ( dom y c= S & dom z c= T ) and
A2: dom y c= dom r and
A3: A c= dom y ; :: thesis: (Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) = Sum (y,z,yz,r,s,S,T)
set P1 = Sum ((y | A),z,yz,(r | A),s,S,T);
set P2 = Sum ((y /^ A),z,yz,(r /^ A),s,S,T);
set P12 = Sum (y,z,yz,r,s,S,T);
A4: ( dom (Sum ((y | A),z,yz,(r | A),s,S,T)) = dom yz & dom yz = dom (Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) & dom yz = dom (Sum (y,z,yz,r,s,S,T)) ) by Def19;
then dom yz = (dom (Sum ((y | A),z,yz,(r | A),s,S,T))) /\ (dom (Sum ((y /^ A),z,yz,(r /^ A),s,S,T))) ;
then A5: dom ((Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T))) = dom yz by VALUED_1:def 1;
for a being object st a in dom yz holds
(Sum (y,z,yz,r,s,S,T)) . a = ((Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T))) . a

proof

let a be object ; :: thesis: ( a in dom yz implies (Sum (y,z,yz,r,s,S,T)) . a = ((Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T))) . a )
assume A6: a in dom yz ; :: thesis: (Sum (y,z,yz,r,s,S,T)) . a = ((Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T))) . a
A7: y = (y | A) ^ (y /^ A) by Def1;
A8: r = (r | A) ^ (r /^ A) by Def1;
A c= dom r by A2, A3;
then A9: ( dom (y | A) = A & dom (r | A) = A ) by A3, RELAT_1:62;
A10: ( dom (y /^ A) = (dom y) -^ A & dom (r /^ A) = (dom r) -^ A ) by Def1;
thus (Sum (y,z,yz,r,s,S,T)) . a = Partial_Sums (y,z,r,s,(yz .. a),S,T) by A6, Def19
.= (Partial_Sums ((y | A),z,(r | A),s,(yz .. a),S,T)) + (Partial_Sums ((y /^ A),z,(r /^ A),s,(yz .. a),S,T)) by A1, A7, A8, A9, A10, A2, ORDINAL3:59, Th86
.= ((Sum ((y | A),z,yz,(r | A),s,S,T)) . a) + (Partial_Sums ((y /^ A),z,(r /^ A),s,(yz .. a),S,T)) by A6, Def19
.= ((Sum ((y | A),z,yz,(r | A),s,S,T)) . a) + ((Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) . a) by A6, Def19
.= ((Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T))) . a by A6, A5, VALUED_1:def 1 ; :: thesis: verum

end;

hence (Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) = Sum (y,z,yz,r,s,S,T) by A4, A5, FUNCT_1:2; :: thesis: verum