theorem :: XCMPLX_1:136

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