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