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:28;
hence cpx2euc (euc2cpx p) = p by EUCLID:57; :: thesis: verum