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