:: deftheorem Def27 defines name-y SURREALC:def 27 :
for x being surreal number
for b₂ being strictly_decreasing uSurreal-Sequence holds
( b₂ = name-y x iff ( dom (name-r x) = dom b₂ & Sum ((name-r x),(No_omega^ b₂)) == x ) );