theorem :: XCMPLX_1:109

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