let m, n, k 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_relative_prime & k,n are_relative_prime ) by INT_2:def 4;
then m * k,n are_relative_prime by INT_2:41;
hence (m * k) gcd n = 1 by INT_2:def 4; :: thesis: verum