theorem :: COMPLFLD:19

for z being Element of F_Complex st z <> 0. F_Complex holds
(- z) " = - (z ")