let z1, z2 be Element of COMPLEX ; :: thesis: ( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) )
thus 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 Def12
.= (Im z1) - (Im z2) by Th28 ; :: thesis: verum