:: deftheorem Def4 defines No_omega_op SURREALC:def 4 :
for A being Ordinal
for b₂ being ManySortedSet of Day A holds
( b₂ = No_omega_op A iff ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & b₂ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) ) );