theorem :: COMPLEX1:37

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