let z1, z2 be Complex; :: thesis: |.z1.| / |.z2.| = |.(z1 / z2).|
thus |.z1.| / |.z2.| = |.z1.| * (|.z2.| ") by XCMPLX_0:def 9
.= |.z1.| * |.(z2 ").| by Th66
.= |.(z1 * (z2 ")).| by Th65
.= |.(z1 / z2).| by XCMPLX_0:def 9 ; :: thesis: verum