theorem :: XCMPLX_1:99

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