let k, m, n be Integer; :: thesis: ( m gcd n = 1 & k gcd n = 1 implies (m * k) gcd n = 1 )
assume ( m gcd n = 1 & k gcd n = 1 ) ; :: thesis: (m * k) gcd n = 1
then ( m,n are_coprime & k,n are_coprime ) by INT_2:def 3;
then m * k,n are_coprime by INT_2:26;
hence (m * k) gcd n = 1 by INT_2:def 3; :: thesis: verum