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,(No_omega^ 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,(No_omega^ 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,(No_omega^ 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, Th98;
A3: dom y = dom (No_omega^ y) by Def22;
set s = Partial_Sums (r,(No_omega^ y));
A4: dom (Partial_Sums (r,(No_omega^ y))) = succ ((succ (card (bool (succ (born_eq x))))) /\ (succ (card (bool (succ (born_eq x)))))) by A3, A2, Def20
.= succ (succ (card (bool (succ (born_eq x))))) ;
Partial_Sums (r,(No_omega^ y)), No_omega^ y,r simplest_up_to dom (Partial_Sums (r,(No_omega^ y))) by Def20;
then Partial_Sums (r,(No_omega^ y)), No_omega^ y,r simplest_up_to succ ((succ (card (bool (succ (born_eq x))))) /\ (succ (card (bool (succ (born_eq x)))))) by A3, A2, Def20;
then rng (born ((Partial_Sums (r,(No_omega^ y))) | (succ (succ (card (bool (succ (born_eq x)))))))) c= succ (born_eq x) by A2, Th91, Th101;
then A5: card (rng (born (Partial_Sums (r,(No_omega^ y))))) c= card (succ (born_eq x)) by A4, CARD_1:11;
born (Partial_Sums (r,(No_omega^ y))) is one-to-one by CARD_5:11;
then A6: card (rng (born (Partial_Sums (r,(No_omega^ y))))) = card (dom (born (Partial_Sums (r,(No_omega^ y))))) by CARD_1:5, WELLORD2:def 4
.= card (succ (succ (card (bool (succ (born_eq x)))))) by A4, Def24 ;
A7: card (succ (succ (card (bool (succ (born_eq x)))))) in card (bool (succ (born_eq x))) by A5, A6, 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 A7, 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
A8: ( dom r = dom y & r,y, dom r name_like x & Sum (r,(No_omega^ 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,(No_omega^ y)) == x )
take y ; :: thesis: ( dom r = dom y & dom y c= born_eq x & Sum (r,(No_omega^ y)) == x )
A9: dom y = dom (No_omega^ y) by Def22;
( born (Sum (r,(No_omega^ y))) = born_eq (Sum (r,(No_omega^ y))) & born_eq (Sum (r,(No_omega^ y))) = born_eq x ) by A8, SURREALO:33, SURREALO:48;
hence ( dom r = dom y & dom y c= born_eq x & Sum (r,(No_omega^ y)) == x ) by A8, A9, Th102; :: thesis: verum