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