theorem Th14: :: SURREALS:14

for S being c=-monotone Function-yielding Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for o being object st o in Day B holds
SB . o = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o)))] ) ) ) holds
for A being Ordinal st A in dom S holds
No_sqrt_op A = S . A