let o be object ; :: thesis:
let x be Surreal; :: thesis:
set A = born x;
deffunc H₁( set , Function-yielding c=-monotone Sequence) -> set = { (((union (rng $2)) . xL) *' (uReal . r)) where xL is Element of $1, r is Element of REAL : ( xL in $1 & r is positive ) } ;
deffunc H₂( object , Function-yielding c=-monotone Sequence) -> object = [({0_No} \/ H₁( L_ $1,$2)),H₁( R_ $1,$2)];
consider S being Function-yielding c=-monotone Sequence such that
A1: ( dom S = succ (born x) & No_omega_op (born x) = S . (born x) ) and
A2: for B being Ordinal st B in succ (born x) holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = H₂(x,S | B) ) ) by Def4;
consider SA being ManySortedSet of Day (born x) such that
A3: S . (born x) = SA and
A4: for x being object st x in Day (born x) holds
SA . x = H₂(x,S | (born x)) by A2, ORDINAL1:6;
x in Day (born x) by SURREAL0:def 18;
then A5: No_omega^ x = H₂(x,S | (born x)) by A1, A3, A4;
hence No_omega^ x is pair ; :: thesis:
A6: for T being surreal-membered set st ( T = L_ x or T = R_ x ) holds
for o being object holds
( o in H₁(T,S | (born x)) iff ex y being Surreal ex r being positive Real st
( y in T & o = (No_omega^ y) *' (uReal . r) ) )

let T be surreal-membered set ; :: thesis:
assume A7: ( T = L_ x or T = R_ x ) ; :: thesis:
let o be object ; :: thesis:
thus ( o in H₁(T,S | (born x)) implies ex y being Surreal ex r being positive Real st
( y in T & o = (No_omega^ y) *' (uReal . r) ) ) :: thesis:

assume o in H₁(T,S | (born x)) ; :: thesis:
then consider a being Element of T, r being Element of REAL such that
A8: ( o = ((union (rng (S | (born x)))) . a) *' (uReal . r) & a in T & r is positive ) ;
reconsider a = a as Surreal by SURREAL0:def 16, A8;
reconsider r = r as positive Real by A8;
take a ; :: thesis:
take r ; :: thesis:
set B = born a;
A9: a in (L_ x) \/ (R_ x) by A7, A8, XBOOLE_0:def 3;
then A10: born a in born x by SURREALO:1;
A11: born a in succ (born x) by A9, SURREALO:1, ORDINAL1:8;
then consider SB being ManySortedSet of Day (born a) such that
A12: ( S . (born a) = SB & ( for x being object st x in Day (born a) holds
SB . x = H₂(x,S | (born a)) ) ) by A2;
A13: dom SB = Day (born a) by PARTFUN1:def 2;
A14: a in Day (born a) by SURREAL0:def 18;
A15: SB . a = (union (rng S)) . a by SURREALR:2, A12, A13, A14, A11, A1;
SB . a = No_omega^ a by A11, A1, A2, Th21, A12;
hence ( a in T & o = (No_omega^ a) *' (uReal . r) ) by SURREALR:5, A10, A13, A14, A12, A8, A15; :: thesis:

end;

end;

thus ( not o in L_ (No_omega^ x) or o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) *' (uReal . r) ) ) :: thesis:

end;

thus ( ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) *' (uReal . r) ) ) implies o in L_ (No_omega^ x) ) :: thesis:

assume ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) *' (uReal . r) ) ) ; :: thesis:

end;

end;

thus ( o in R_ (No_omega^ x) implies ex xL being Surreal ex r being positive Real st
( xL in R_ x & o = (No_omega^ xL) *' (uReal . r) ) ) by A5, A6; :: thesis:
assume ex xL being Surreal ex r being positive Real st
( xL in R_ x & o = (No_omega^ xL) *' (uReal . r) ) ; :: thesis:
hence o in R_ (No_omega^ x) by A5, A6; :: thesis: