theorem :: XCMPLX_1:76

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