let r1, r2 be non-zero Sequence of REAL ; :: thesis: for y1, y2 being strictly_decreasing uSurreal-Sequence st dom r1 = dom y1 & dom r2 = dom y2 & Sum (r1,y1) == Sum (r2,y2) holds
( r1 = r2 & y1 = y2 )
let y1, y2 be strictly_decreasing uSurreal-Sequence; :: thesis: ( dom r1 = dom y1 & dom r2 = dom y2 & Sum (r1,y1) == Sum (r2,y2) implies ( r1 = r2 & y1 = y2 ) )
assume A1: ( dom r1 = dom y1 & dom r2 = dom y2 & Sum (r1,y1) == Sum (r2,y2) ) ; :: thesis: ( r1 = r2 & y1 = y2 )
A2: Sum (r1,y1) = Sum (r2,y2) by A1, SURREALO:50;
A3: r1,y1, dom r1 name_like Sum (r1,y1) by Th101, A1;
A4: r2,y2, dom r2 name_like Sum (r2,y2) by Th101, A1;

per cases ( dom r1 in dom r2 or dom r1 = dom r2 or dom r2 in dom r1 ) by ORDINAL1:14;

suppose A5: dom r1 in dom r2 ; :: thesis: ( r1 = r2 & y1 = y2 )

then A6: dom r1 c= dom r2 by ORDINAL1:def 2;
r2,y2, dom r1 name_like Sum (r2,y2) by A4, A6;
then A7: ( r1 | (dom r1) = r2 | (dom r1) & y1 | (dom r1) = y2 | (dom r1) ) by A3, A2, Th87;
set s = Partial_Sums (r2,y2);
(Partial_Sums (r2,y2)) . (dom r1) = ((Partial_Sums (r2,y2)) | (succ (dom r1))) . (dom r1) by FUNCT_1:49, ORDINAL1:6
.= (Partial_Sums ((r2 | (dom r1)),(y2 | (dom r1)))) . (dom r1) by Th85
.= Sum (r1,y1) by A1, A7 ;
hence ( r1 = r2 & y1 = y2 ) by A1, A4, A5; :: thesis: verum

end;

suppose A8: dom r1 = dom r2 ; :: thesis: ( r1 = r2 & y1 = y2 )

r2,y2, dom r1 name_like Sum (r2,y2) by Th101, A1, A8;
then ( r1 = r1 | (dom r1) & r1 | (dom r1) = r2 | (dom r1) & r2 | (dom r1) = r2 & y1 = y1 | (dom r1) & y1 | (dom r1) = y2 | (dom r1) & y2 | (dom r1) = y2 ) by A8, A3, A2, Th87;
hence ( r1 = r2 & y1 = y2 ) ; :: thesis: verum

end;

suppose A9: dom r2 in dom r1 ; :: thesis: ( r1 = r2 & y1 = y2 )

then A10: dom r2 c= dom r1 by ORDINAL1:def 2;
r1,y1, dom r2 name_like Sum (r1,y1) by A10, A3;
then A11: ( r1 | (dom r2) = r2 | (dom r2) & y1 | (dom r2) = y2 | (dom r2) ) by A4, A2, Th87;
set s = Partial_Sums (r1,y1);
(Partial_Sums (r1,y1)) . (dom r2) = ((Partial_Sums (r1,y1)) | (succ (dom r2))) . (dom r2) by ORDINAL1:6, FUNCT_1:49
.= (Partial_Sums ((r1 | (dom r2)),(y1 | (dom r2)))) . (dom r2) by Th85
.= Sum (r2,y2) by A1, A11 ;
hence ( r1 = r2 & y1 = y2 ) by A1, A3, A9; :: thesis: verum

end;

end;