theorem Th3: :: RING_3:3

multcomplex || REAL = multreal