:: deftheorem Def6 defines No_sqrt_op SURREALS:def 6 :
for A being Ordinal
for b₂ being ManySortedSet of Day A holds
( b₂ = No_sqrt_op A iff ex S being c=-monotone Function-yielding 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 = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x)))] ) ) ) ) );