:: deftheorem Def6 defines No_sum_op SURREALR:def 6 :
for A being Ordinal
for b₂ being ManySortedSet of Triangle A holds
( b₂ = No_sum_op A iff ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & b₂ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [((union (rng (S | B))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | B))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] ) ) ) ) );