let z1, z2 be Complex; :: thesis: cpx2euc (z1 + z2) = (cpx2euc z1) + (cpx2euc z2)
(cpx2euc z1) + (cpx2euc z2) = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]| by EUCLID:56;
hence cpx2euc (z1 + z2) = (cpx2euc z1) + (cpx2euc z2) by Th6; :: thesis: verum