theorem Th117: :: XCMPLX_1:117
for a, b being Complex st a <> 0 holds
a + b = a * (1 + (b / a))