theorem :: XCMPLX_1:103

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