theorem Th57: :: SURREALN:57
for r1, r2 being Real holds (uReal . r1) * (uReal . r2) == uReal . (r1 * r2)