theorem Th69: :: SURREALC:69
for y being Surreal
for r being Real
for s being Surreal st r <> 0 holds
s + ((uReal . r) * (No_omega^ y)) is s,y,r _term