theorem Th8: :: COMPLEX1:8
for z1, z2 being Complex holds
( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )