theorem :: XCMPLX_1:17

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