theorem :: XCMPLX_1:98

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