theorem :: XCMPLX_1:70

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