theorem :: EUCLID_3:24

for z being Complex holds |.(cpx2euc z).| = sqrt (((Re z) ^2) + ((Im z) ^2))