let m be Integer; :: thesis: for p being Rational st m <> 0 holds
p = ((numerator p) * m) / ((denominator p) * m)
let p be Rational; :: thesis: ( m <> 0 implies p = ((numerator p) * m) / ((denominator p) * m) )
assume m <> 0 ; :: thesis: p = ((numerator p) * m) / ((denominator p) * m)
then (numerator p) / (denominator p) = ((numerator p) * m) / ((denominator p) * m) by XCMPLX_1:91;
hence p = ((numerator p) * m) / ((denominator p) * m) by Th12; :: thesis: verum