theorem :: XCMPLX_1:107

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