theorem Th19: :: RING_3:19

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