theorem Th5: :: EULER_1:5

for a, b being Nat st a gcd b = 1 holds
for c being Nat holds (a * c) gcd (b * c) = c