theorem Th65: :: COMPLEX1:65

for z1, z2 being Complex holds |.(z1 * z2).| = |.z1.| * |.z2.|