theorem Th102: :: SURREALC:102
for r1, r2 being non-zero Sequence of REAL
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 )