let z be Complex; :: thesis: euc2cpx (cpx2euc z) = z
( |[(Re z),(Im z)]| `1 = Re z & |[(Re z),(Im z)]| `2 = Im z ) by EUCLID:52;
hence euc2cpx (cpx2euc z) = z by COMPLEX1:13; :: thesis: verum