theorem :: XCMPLX_1:28

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