:: deftheorem Def23 defines name-y SURREALC:def 23 :
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),b₂) == x ) );