theorem :: COMPLFLD:52

for z being Element of F_Complex holds (- z) *' = - (z *') by COMPLEX1:33;