let z be Element of F_Complex; :: thesis: ( z <> 0. F_Complex implies |.(z ").| = |.z.| " )
reconsider z1 = z as Element of COMPLEX by Def1;
assume z <> 0. F_Complex ; :: thesis: |.(z ").| = |.z.| "
then z " = z1 " by Th5;
hence |.(z ").| = |.z.| " by COMPLEX1:66; :: thesis: verum