let i, j, k be Integer; :: thesis: ( i,j are_coprime implies i gcd (j * k) = i gcd k )
assume A1: i gcd j = 1 ; :: according to INT_2:def 3 :: thesis: i gcd (j * k) = i gcd k
(i * k) gcd (j * k) = |.k.| * (i gcd j) by Th16;
then i gcd |.k.| = (i gcd (i * k)) gcd (j * k) by A1, Th18
.= |.i.| gcd (j * k) by Th17
.= (j * k) gcd i by Th14 ;
hence i gcd (j * k) = i gcd k by Th14; :: thesis: verum