theorem :: COMPLFLD:30

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