:: deftheorem Def11 defines No_Ordinal_op SURREALN:def 11 :
for A being Ordinal
for b₂ being set holds
( b₂ = No_Ordinal_op A iff ex S being Sequence st
( b₂ = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) );