theorem Th71: :: SURREALC:71

for x, y being Surreal
for r being Real
for s being Surreal st r <> 0 holds
( (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term iff |.x.| infinitely< No_omega^ y )