let z be Complex; :: 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:52;
hence |.(cpx2euc z).| = sqrt (((Re z) ^2) + ((Im z) ^2)) by JGRAPH_3:1; :: thesis: verum