theorem :: XCMPLX_1:65

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