reconsider Rz1 = Re z1, Iz1 = Im z1 as Rational ;
reconsider Rz2 = Re z2, Iz2 = Im z2 as Rational ;
( Re (z1 * z2) = (Rz1 * Rz2) - (Iz1 * Iz2) & Im (z1 * z2) = (Rz1 * Iz2) + (Rz2 * Iz1) ) by COMPLEX1:9;
hence z1 * z2 is g_rational by RAT_1:def 2; :: thesis: verum