let p be Point of (TOP-REAL 2); :: thesis: |.(euc2cpx p).| = sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 ))
Re (euc2cpx p) = p `1 by COMPLEX1:28;
hence |.(euc2cpx p).| = sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 )) by COMPLEX1:28; :: thesis: verum