theorem :: XCMPLX_1:27

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