theorem :: XCMPLX_1:179

for a being Complex holds (- 1) * a = - a ;