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