let p be Point of (TOP-REAL 2); :: thesis: cpx2euc (euc2cpx p) = p
( Re ((p `1) + ((p `2) * <i>)) = p `1 & Im ((p `1) + ((p `2) * <i>)) = p `2 ) by COMPLEX1:12;
hence cpx2euc (euc2cpx p) = p by EUCLID:53; :: thesis: verum