:: deftheorem defines name_like SURREALC:def 19 :
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for alpha being Ordinal
for x being Surreal holds
( r,y,alpha name_like x iff ( alpha c= dom r & dom r = dom y & ( for beta being Ordinal st beta in alpha holds
for Pb being Surreal st Pb = (Partial_Sums (r,y)) . beta holds
( not x == Pb & r . beta = omega-r (x - Pb) & y . beta = omega-y (x - Pb) ) ) ) );