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