let z be complex number ; :: thesis: euc2cpx (cpx2euc z) = z
( |[(Re z),(Im z)]| `1 = Re z & |[(Re z),(Im z)]| `2 = Im z ) by EUCLID:56;
hence euc2cpx (cpx2euc z) = z by COMPLEX1:29; :: thesis: verum