theorem Th115: :: XCMPLX_1:115

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