theorem Th16: :: INT_6:16

for i, j, k being Integer holds (i * j) gcd (i * k) = |.i.| * (j gcd k)