let a, b, c be Integer; :: thesis: ( a,c are_coprime & b,c are_coprime implies a * b,c are_coprime )
assume that
A1: a,c are_coprime and
A2: b,c are_coprime ; :: thesis: a * b,c are_coprime
A4: ((a * b) gcd c) gcd a divides a by Def2;
A5: (a * b) gcd c divides c by Def2;
((a * b) gcd c) gcd a divides (a * b) gcd c by Def2;
then ((a * b) gcd c) gcd a divides c by A5, Lm2;
then ((a * b) gcd c) gcd a divides 1 by A1, A4, Def2;
then a,(a * b) gcd c are_coprime by INT_1:9;
then (a * b) gcd c divides b by Th21, Th25;
then (a * b) gcd c divides 1 by A2, A5, Def2;
hence a * b,c are_coprime by INT_1:9; :: thesis: verum