theorem :: XCMPLX_1:100

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