theorem :: XCMPLX_1:137

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