theorem :: COMPLFLD:73

for z1, z2 being Element of F_Complex st z2 <> 0. F_Complex holds
|.z1.| / |.z2.| = |.(z1 / z2).|