let m, n be Integer; :: thesis: for p being Rational st p = m / n & n <> 0 holds
ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )
let p be Rational; :: thesis: ( p = m / n & n <> 0 implies ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 ) )
assume A1: ( p = m / n & n <> 0 ) ; :: thesis: ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )

per cases ( n < 0 or 0 < n ) by A1;

suppose n < 0 ; :: thesis: ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )

then 0 <= - n ;
then reconsider x = - n as Element of NAT by INT_1:16;
A2: x <> 0 by A1;
p = - ((- m) / n) by A1
.= (- m) / x by XCMPLX_1:189 ;
then consider k being Element of NAT such that
A3: ( - m = (numerator p) * k & x = (denominator p) * k ) by A2, Th60;
take y = - k; :: thesis: ( m = (numerator p) * y & n = (denominator p) * y )
thus m = - ((numerator p) * k) by A3
.= (numerator p) * y ; :: thesis: n = (denominator p) * y
thus n = - ((denominator p) * k) by A3
.= (denominator p) * y ; :: thesis: verum

end;

suppose 0 < n ; :: thesis: ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )

then reconsider x = n as Element of NAT by INT_1:16;
consider k being Element of NAT such that
A4: ( m = (numerator p) * k & x = (denominator p) * k ) by A1, Th60;
reconsider y = k as Integer ;
take y ; :: thesis: ( m = (numerator p) * y & n = (denominator p) * y )
thus ( m = (numerator p) * y & n = (denominator p) * y ) by A4; :: thesis: verum

end;

end;