:: deftheorem Def11 defines No_inverse_op SURREALI:def 11 :
for A being Ordinal
for b₂ being ManySortedSet of Positives A holds
( b₂ = No_inverse_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 Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) ) );