let p be Rational; :: thesis: ( p = (numerator p) / (denominator p) & p = (numerator p) * ((denominator p) ") )
set x = denominator p;
thus (numerator p) / (denominator p) = p * ((denominator p) * ((denominator p) "))
.= p * 1 by XCMPLX_0:def 7
.= p ; :: thesis: p = (numerator p) * ((denominator p) ")
hence p = (numerator p) * ((denominator p) ") ; :: thesis: verum