for z1, z2 being Element of F_Complex holds |.(z1 * z2).| = |.z1.| * |.z2.| by COMPLEX1:65;