theorem :: XCMPLX_1:25

for a, b being Complex holds a = a + (b - b) ;