theorem :: XCMPLX_1:91

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