let z be complex number ; :: thesis: |.(cpx2euc z).| = sqrt (((Re z) ^2) + ((Im z) ^2))
( |[(Re z),(Im z)]| `1 = Re z & |[(Re z),(Im z)]| `2 = Im z ) by EUCLID:56;
hence |.(cpx2euc z).| = sqrt (((Re z) ^2) + ((Im z) ^2)) by JGRAPH_3:10; :: thesis: verum