theorem :: XCMPLX_1:176

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