let p be Rational; :: thesis: ( p <> 0 implies denominator p = (numerator p) / p )
assume A1: p <> 0 ; :: thesis: denominator p = (numerator p) / p
((p " ) * p) * (denominator p) = (p " ) * (numerator p) ;
then 1 * (denominator p) = (p " ) * (numerator p) by A1, XCMPLX_0:def 7;
hence denominator p = (numerator p) / p ; :: thesis: verum