theorem Th55: :: SURREALN:55
for r1, r2 being Real holds (uReal . r1) + (uReal . r2) == uReal . (r1 + r2)