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