theorem Th32: :: COMPLEX1:32

for z1, z2 being Complex holds (z1 + z2) *' = (z1 *') + (z2 *')