let y1, y2 be strictly_decreasing uSurreal-Sequence; :: thesis: ( dom (name-r x) = dom y1 & Sum ((name-r x),y1) == x & dom (name-r x) = dom y2 & Sum ((name-r x),y2) == x implies y1 = y2 )
assume that
A2: ( dom (name-r x) = dom y1 & Sum ((name-r x),y1) == x ) and
A3: ( dom (name-r x) = dom y2 & Sum ((name-r x),y2) == x ) ; :: thesis: y1 = y2
Sum ((name-r x),y1) == Sum ((name-r x),y2) by A2, A3, SURREALO:10;
hence y1 = y2 by A2, A3, Th102; :: thesis: verum