let x be Surreal; :: thesis: ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( dom r = dom y & dom y c= born_eq x & Sum (r,y) == x )
ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( dom r = dom y & r,y, dom r name_like x & Sum (r,y) == x )

proof

assume A1: for r being non-zero Sequence of REAL
for y being strictly_decreasing uSurreal-Sequence st dom r = dom y & r,y, dom r name_like x holds
not Sum (r,y) == x ; :: thesis: contradiction
set b = card (bool (succ (born_eq x)));
consider r being non-zero Sequence of REAL , y being strictly_decreasing uSurreal-Sequence such that
A2: ( dom r = succ (card (bool (succ (born_eq x)))) & succ (card (bool (succ (born_eq x)))) = dom y & r,y, succ (card (bool (succ (born_eq x)))) name_like x ) by A1, Th95;
set s = Partial_Sums (r,y);
A3: dom (Partial_Sums (r,y)) = succ ((succ (card (bool (succ (born_eq x))))) /\ (succ (card (bool (succ (born_eq x)))))) by A2, Def17
.= succ (succ (card (bool (succ (born_eq x))))) ;
Partial_Sums (r,y),y,r simplest_up_to dom (Partial_Sums (r,y)) by Def17;
then Partial_Sums (r,y),y,r simplest_up_to succ ((succ (card (bool (succ (born_eq x))))) /\ (succ (card (bool (succ (born_eq x)))))) by A2, Def17;
then rng (born ((Partial_Sums (r,y)) | (succ (succ (card (bool (succ (born_eq x)))))))) c= succ (born_eq x) by A2, Th88, Th98;
then A4: card (rng (born (Partial_Sums (r,y)))) c= card (succ (born_eq x)) by A3, CARD_1:11;
born (Partial_Sums (r,y)) is one-to-one by CARD_5:11;
then A5: card (rng (born (Partial_Sums (r,y)))) = card (dom (born (Partial_Sums (r,y)))) by CARD_1:5, WELLORD2:def 4
.= card (succ (succ (card (bool (succ (born_eq x)))))) by A3, Def20 ;
A6: card (succ (succ (card (bool (succ (born_eq x)))))) in card (bool (succ (born_eq x))) by A4, A5, CARD_1:14, ORDINAL1:12;
card (bool (succ (born_eq x))) in succ (succ (card (bool (succ (born_eq x))))) by ORDINAL1:6, ORDINAL1:8;
then card (bool (succ (born_eq x))) c= succ (succ (card (bool (succ (born_eq x))))) by ORDINAL1:def 2;
then ( card (bool (succ (born_eq x))) = card (card (bool (succ (born_eq x)))) & card (card (bool (succ (born_eq x)))) in card (bool (succ (born_eq x))) ) by A6, ORDINAL1:12, CARD_1:11;
hence contradiction ; :: thesis: verum

end;

then consider r being non-zero Sequence of REAL , y being strictly_decreasing uSurreal-Sequence such that
A7: ( dom r = dom y & r,y, dom r name_like x & Sum (r,y) == x ) ;
take r ; :: thesis: ex y being strictly_decreasing uSurreal-Sequence st
( dom r = dom y & dom y c= born_eq x & Sum (r,y) == x )
take y ; :: thesis: ( dom r = dom y & dom y c= born_eq x & Sum (r,y) == x )
( born (Sum (r,y)) = born_eq (Sum (r,y)) & born_eq (Sum (r,y)) = born_eq x ) by A7, SURREALO:33, SURREALO:48;
hence ( dom r = dom y & dom y c= born_eq x & Sum (r,y) == x ) by A7, Th99; :: thesis: verum