theorem Th21: :: SURREALC:21

for S being Function-yielding c=-monotone Sequence st ( for B being Ordinal st B in dom S 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 ) } ] ) ) ) holds
for A being Ordinal st A in dom S holds
No_omega_op A = S . A