theorem Th40: :: SURREALN:40
for d1, d2 being Dyadic holds (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)