theorem :: XCMPLX_1:89

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