theorem Th2: :: RING_3:2

addcomplex || REAL = addreal