theorem :: XCMPLX_1:64

for a being Complex holds (a + a) / 2 = a ;