( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) ) by COMPLEX1:19;
hence z1 - z2 is g_integer by INT_1:def 2; :: thesis: verum