( Re (z1 + z2) = (Re z1) + (Re z2) & Re z2 = 0 ) by Def3, COMPLEX1:8;
hence z1 + z2 is imaginary by Def3; :: thesis: verum