theorem Th27: :: RING_3:27

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