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