theorem :: XCMPLX_1:84

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