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:12;
hence |.(euc2cpx p).| = sqrt (((p `1) ^2) + ((p `2) ^2)) by COMPLEX1:12; :: thesis: verum