theorem :: XCMPLX_1:40

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