theorem :: XCMPLX_1:88

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