theorem :: XCMPLX_1:85

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