let a, b, c be Integer; :: thesis: ( a <> 0 & c <> 0 & a,c are_coprime & b,c are_coprime implies a * b,c are_coprime )
assume A1: ( a <> 0 & c <> 0 ) ; :: thesis: ( not a,c are_coprime or not b,c are_coprime or a * b,c are_coprime )
assume a,c are_coprime ; :: thesis: ( not b,c are_coprime or a * b,c are_coprime )
then A2: |.a.|,|.c.| are_coprime by INT_2:34;
assume b,c are_coprime ; :: thesis: a * b,c are_coprime
then |.b.|,|.c.| are_coprime by INT_2:34;
then A3: |.a.| * |.b.|,|.c.| are_coprime by A1, A2, EULER_1:14;
|.a.| * |.b.| = |.(a * b).| by COMPLEX1:65;
hence a * b,c are_coprime by A3, INT_2:34; :: thesis: verum