theorem :: COMPLFLD:10

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