theorem Th27: :: SURREALC:27

for x, y being Surreal holds (No_omega^ x) * (No_omega^ y) == No_omega^ (x + y)