theorem :: XCMPLX_1:13

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