theorem Th9: :: COMPLEX1:9

for z1, z2 being Complex holds
( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )