theorem Th15: :: RING_3:15

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