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 that
A1: p = m / n and
A2: n <> 0 ; :: thesis: ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )

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

suppose n < 0 ; :: 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:3;
A3: p = - ((- m) / n) by A1
.= (- m) / x by XCMPLX_1:188 ;
x <> 0 by A2;
then consider k being Nat such that
A4: - m = (numerator p) * k and
A5: x = (denominator p) * k by A3, Th24;
take y = - k; :: thesis: ( m = (numerator p) * y & n = (denominator p) * y )
thus m = - ((numerator p) * k) by A4
.= (numerator p) * y ; :: thesis: n = (denominator p) * y
thus n = - ((denominator p) * k) by A5
.= (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:3;
consider k being Nat such that
A6: m = (numerator p) * k and
A7: x = (denominator p) * k by A1, A2, Th24;
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 A6, A7; :: thesis: verum

end;

end;