:: deftheorem Def12 defines No_mult_op SURREALR:def 12 :
for A being Ordinal
for b₂ being ManySortedSet of Triangle A holds
( b₂ = No_mult_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))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) ) );