( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) ) by COMPLEX1:20;
hence z " is g_rational by RAT_1:def 2; :: thesis: verum