theorem :: XCMPLX_1:132

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