theorem Th211: :: XCMPLX_1:211

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