theorem Th14: :: RING_3:14

for m being Nat
for i being Integer st m <> 0 holds
(i div (i gcd m)) gcd (m div (i gcd m)) = 1