theorem :: XCMPLX_1:11

for a being Complex holds 2 * a = a + a ;