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