theorem :: XCMPLX_1:233
for a, b, c, d, e being Complex holds a / ((b * c) * (d / e)) = (e / c) * (a / (b * d))