theorem :: XCMPLX_1:12

for a being Complex holds 3 * a = (a + a) + a ;