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 Th7;
hence |.(z " ).| = |.z.| " by COMPLEX1:152; :: thesis: verum