theorem Th25: :: SURREALI:25

for S being c=-monotone Function-yielding Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for o being object st o in Positives B holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | B)))))),(Union (divR (||.o.||,(union (rng (S | B))))))] ) ) ) holds
for A being Ordinal st A in dom S holds
No_inverse_op A = S . A