let z1, z2 be complex number ; :: thesis: ( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) )
A1: ( z1 in COMPLEX & z2 in COMPLEX ) by XCMPLX_0:def 2;
hence Re (z1 - z2) = Re (((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>)) by Def12
.= (Re z1) - (Re z2) by Th28 ;
:: thesis: Im (z1 - z2) = (Im z1) - (Im z2)
thus Im (z1 - z2) = Im (((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>)) by A1, Def12
.= (Im z1) - (Im z2) by Th28 ; :: thesis: verum