for m being Nat
for i being Integer st m <> 0 holds
( denominator ((m / i) ") = m / (m gcd i) & numerator ((m / i) ") = i / (m gcd i) )