let p be Rational; :: thesis: ( p = (numerator p) / (denominator p) & p = (numerator p) * ((denominator p) " ) & p = ((denominator p) " ) * (numerator p) )
set x = denominator p;
A1: denominator p <> 0 by Def3;
thus A2: (numerator p) / (denominator p) = p * ((denominator p) * ((denominator p) " ))
.= p * 1 by A1, XCMPLX_0:def 7
.= p ; :: thesis: ( p = (numerator p) * ((denominator p) " ) & p = ((denominator p) " ) * (numerator p) )
hence p = (numerator p) * ((denominator p) " ) ; :: thesis: p = ((denominator p) " ) * (numerator p)
thus p = ((denominator p) " ) * (numerator p) by A2; :: thesis: verum