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