theorem Th35: :: COMPLEX1:35

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