let r1, r2 be non-zero Sequence of REAL ; :: thesis: ( ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom r1 & Sum (r1,y) == x ) & ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom r2 & Sum (r2,y) == x ) implies r1 = r2 )
given y1 being strictly_decreasing uSurreal-Sequence such that A2: ( dom y1 = dom r1 & Sum (r1,y1) == x ) ; :: thesis: ( for y being strictly_decreasing uSurreal-Sequence holds
( not dom y = dom r2 or not Sum (r2,y) == x ) or r1 = r2 )
given y2 being strictly_decreasing uSurreal-Sequence such that A3: ( dom y2 = dom r2 & Sum (r2,y2) == x ) ; :: thesis: r1 = r2
Sum (r1,y1) == Sum (r2,y2) by A2, A3, SURREALO:10;
hence r1 = r2 by A2, A3, Th102; :: thesis: verum