let z1, z2 be 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 Lm23
.= (Re z1) - (Re z2) by Th12 ; :: thesis: Im (z1 - z2) = (Im z1) - (Im z2)
thus Im (z1 - z2) = Im (((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>)) by Lm23
.= (Im z1) - (Im z2) by Th12 ; :: thesis: verum