let p be Rational; :: thesis: for m, n being Nat st m = denominator p & n = numerator p & n <> 0 holds
( denominator (p ") = n div (n gcd m) & numerator (p ") = m div (n gcd m) )
let m, n be Nat; :: thesis: ( m = denominator p & n = numerator p & n <> 0 implies ( denominator (p ") = n div (n gcd m) & numerator (p ") = m div (n gcd m) ) )
assume ( m = denominator p & n = numerator p ) ; :: thesis: ( not n <> 0 or ( denominator (p ") = n div (n gcd m) & numerator (p ") = m div (n gcd m) ) )
then p = n / m by RAT_1:15;
hence ( not n <> 0 or ( denominator (p ") = n div (n gcd m) & numerator (p ") = m div (n gcd m) ) ) by Th19; :: thesis: verum