for p being Rational holds
( numerator p = 0 iff p = 0 ) by XCMPLX_1:6;