theorem :: XCMPLX_1:74

for a, b, c being Complex holds a * (b / c) = (a * b) / c by Lm8;