theorem :: COMPLFLD:52

for z being Element of F_Complex holds (- z) *' = - (z *')