let x be Surreal; :: thesis:
let r be non-zero Sequence of REAL ; :: thesis:
let y be strictly_decreasing Surreal-Sequence; :: thesis:
let s be uSurreal-Sequence; :: thesis:
let A be Ordinal; :: thesis:
assume A1: ( A c= dom r & x in_meets_terms s,y,r,A & s,y,r simplest_up_to succ A ) ; :: thesis:
let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: o in rng (born (s | (succ A))) ; :: thesis:
consider a being object such that
A3: ( a in dom (born (s | (succ A))) & (born (s | (succ A))) . a = o ) by A2, FUNCT_1:def 3;
reconsider a = a as Ordinal by A3;
A4: a in dom (s | (succ A)) by A3, Def20;
then ( a in dom s & a in succ A ) by RELAT_1:57;
then s . a in rng s by FUNCT_1:def 3;
then reconsider sa = s . a as Surreal by SURREAL0:def 16;
sa = (s | (succ A)) . a by A4, FUNCT_1:47;
then A5: o = born sa by A3, A4, Def20;
A6: a c= A by A4, ORDINAL1:22;
then A7: x in_meets_terms s,y,r,a by A1;
Unique_No x == x by SURREALO:def 10;
then A8: Unique_No x in_meets_terms s,y,r,a by A7, A1, A6, XBOOLE_1:1, Th81;
A9: s,y,r simplest_on_position a by A1, A4;
A10: ( born (Unique_No x) = born_eq (Unique_No x) & born_eq (Unique_No x) = born_eq x ) by SURREALO:33, SURREALO:48, SURREALO:def 10;

per cases ;

suppose a = 0 ; :: thesis:

then sa = 0_No by A9;
then ( born sa = 0 & 0 c= born_eq x ) by SURREAL0:37;
hence o in succ (born_eq x) by A5, ORDINAL1:22; :: thesis:

end;

suppose ( a <> 0 & Unique_No x = sa ) ; :: thesis:

hence o in succ (born_eq x) by A10, ORDINAL1:8, A5; :: thesis:

end;

suppose ( a <> 0 & Unique_No x <> sa ) ; :: thesis:

then born sa in born (Unique_No x) by A8, A9;
hence o in succ (born_eq x) by A5, A10, ORDINAL1:8; :: thesis:

end;

end;