theorem :: XCMPLX_1:108

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