theorem :: XCMPLX_1:93

for a, b, c being Complex st b <> 0 holds
a * c = (a * b) / (b / c)