let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing uSurreal-Sequence
for x being Surreal st dom r = dom y & Sum (r,y) == x holds
name-ord x = dom r
let y be strictly_decreasing uSurreal-Sequence; :: thesis: for x being Surreal st dom r = dom y & Sum (r,y) == x holds
name-ord x = dom r
let x be Surreal; :: thesis: ( dom r = dom y & Sum (r,y) == x implies name-ord x = dom r )
assume A1: ( dom r = dom y & Sum (r,y) == x ) ; :: thesis: name-ord x = dom r
consider r1 being non-zero Sequence of REAL , y1 being strictly_decreasing uSurreal-Sequence such that
A2: ( name-ord x = dom r1 & dom r1 = dom y1 & Sum (r1,y1) == x ) by Def21;
Sum (r1,y1) == Sum (r,y) by A1, A2, SURREALO:10;
hence name-ord x = dom r by A1, A2, Th102; :: thesis: verum