:: deftheorem Def9 defines unique_No_op SURREALO:def 9 :
for A being Ordinal
for b₂ being Sequence holds
( b₂ = unique_No_op A iff ( dom b₂ = succ A & ( for B being Ordinal st B in succ A holds
( b₂ . B c= Day B & ( for x being Surreal holds
( x in b₂ . B iff ( x in union (rng (b₂ | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (b₂ | B)))) & x = the b₅ -smallest Surreal ) ) ) ) ) ) ) ) );