theorem :: XCMPLX_1:77

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