theorem :: XCMPLX_1:26

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