theorem Th17: :: INT_6:17

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