theorem :: XCMPLX_1:87

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