let i, j, k be Integer; :: thesis: ( i,j are_relative_prime implies i gcd (j * k) = i gcd k )
assume AS: i gcd j = 1 ; :: according to INT_2:def 4 :: thesis: i gcd (j * k) = i gcd k
(i * k) gcd (j * k) = (abs k) * (i gcd j) by thgcd0;
then i gcd (abs k) = (i gcd (i * k)) gcd (j * k) by AS, thgcd3
.= (abs i) gcd (j * k) by thgcd4
.= (j * k) gcd i by thagcd ;
hence i gcd (j * k) = i gcd k by thagcd; :: thesis: verum