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,(No_omega^ y1)) == Sum (r2,(No_omega^ 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,(No_omega^ y1)) == Sum (r2,(No_omega^ y2)) implies ( r1 = r2 & y1 = y2 ) )
assume A1: ( dom r1 = dom y1 & dom r2 = dom y2 & Sum (r1,(No_omega^ y1)) == Sum (r2,(No_omega^ y2)) ) ; :: thesis: ( r1 = r2 & y1 = y2 )
A2: Sum (r1,(No_omega^ y1)) = Sum (r2,(No_omega^ y2)) by A1, SURREALO:50;
A3: r1,y1, dom r1 name_like Sum (r1,(No_omega^ y1)) by Th104, A1;
A4: r2,y2, dom r2 name_like Sum (r2,(No_omega^ y2)) by Th104, 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,(No_omega^ y2)) by A4, A6;
then A7: ( r1 | (dom r1) = r2 | (dom r1) & y1 | (dom r1) = y2 | (dom r1) ) by A3, A2, Th90;
set s = Partial_Sums (r2,(No_omega^ y2));
(Partial_Sums (r2,(No_omega^ y2))) . (dom r1) = ((Partial_Sums (r2,(No_omega^ y2))) | (succ (dom r1))) . (dom r1) by FUNCT_1:49, ORDINAL1:6
.= (Partial_Sums ((r2 | (dom r1)),((No_omega^ y2) | (dom r1)))) . (dom r1) by Th87
.= (Partial_Sums (r1,(No_omega^ y1))) . ((dom r1) /\ (dom y1)) by A1, A7, Th88
.= Sum (r1,(No_omega^ y1)) by Def22 ;
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,(No_omega^ y2)) by Th104, 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, Th90;
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,(No_omega^ y1)) by A10, A3;
then A11: ( r1 | (dom r2) = r2 | (dom r2) & y1 | (dom r2) = y2 | (dom r2) ) by A4, A2, Th90;
set s = Partial_Sums (r1,(No_omega^ y1));
(Partial_Sums (r1,(No_omega^ y1))) . (dom r2) = ((Partial_Sums (r1,(No_omega^ y1))) | (succ (dom r2))) . (dom r2) by ORDINAL1:6, FUNCT_1:49
.= (Partial_Sums ((r1 | (dom r2)),((No_omega^ y1) | (dom r2)))) . (dom r2) by Th87
.= (Partial_Sums (r2,(No_omega^ y2))) . ((dom r2) /\ (dom y2)) by A1, A11, Th88
.= Sum (r2,(No_omega^ y2)) by Def22 ;
hence ( r1 = r2 & y1 = y2 ) by A1, A3, A9; :: thesis: verum

end;

end;