theorem Th1: :: EUCLID_3:1

for z being Complex holds euc2cpx (cpx2euc z) = z