consider r being non-zero Sequence of REAL , y being strictly_decreasing uSurreal-Sequence such that
A1: ( dom r = dom y & dom y c= born_eq x & Sum (r,y) == x ) by Th100;
take dom y ; :: thesis: ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom r & dom r = dom y & Sum (r,y) == x )
thus ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom r & dom r = dom y & Sum (r,y) == x ) by A1; :: thesis: verum