theorem :: COMPLFLD:16

for z1, z2, z3 being Element of F_Complex st z2 <> 0. F_Complex & ( z1 * z2 = z3 or z2 * z1 = z3 ) holds
( z1 = z3 * (z2 ") & z1 = (z2 ") * z3 )