theorem :: COMPLFLD:36

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