theorem :: SURREALC:97

for x, z being Surreal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st x in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & z in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & not x == z holds
for A being Ordinal
for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
No_omega^ (omega-y (x - z)) < yA