theorem :: XCMPLX_1:177

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