theorem :: XCMPLX_1:102

for a, b being Complex holds (1 / a) * (1 / b) = 1 / (a * b)