theorem :: XCMPLX_1:110

for a, b being Complex st b <> 0 holds
a = a / (b * (1 / b))