theorem :: XCMPLX_1:220

for a, b, c being Complex holds (a ") * (c / b) = c / (a * b)