let z1, z2 be Element of F_Complex; :: thesis: ( z2 <> 0. F_Complex implies |.z1.| / |.z2.| = |.(z1 / z2).| )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
assume z2 <> 0. F_Complex ; :: thesis: |.z1.| / |.z2.| = |.(z1 / z2).|
then z19 / z29 = z1 / z2 by Th6;
hence |.z1.| / |.z2.| = |.(z1 / z2).| by COMPLEX1:67; :: thesis: verum