theorem :: XCMPLX_1:174

for a, b being Complex holds (- a) * b = - (a * b) ;