let a, b, c, d be Integer; :: thesis: ( a divides b & c divides d implies a * c divides b * d )
assume ( a divides b & c divides d ) ; :: thesis: a * c divides b * d
then ( |.a.| divides |.b.| & |.c.| divides |.d.| ) by INT_2:16;
then A2: |.a.| * |.c.| divides |.b.| * |.d.| by NAT_3:1;
( |.(a * c).| = |.a.| * |.c.| & |.(b * d).| = |.b.| * |.d.| ) by COMPLEX1:65;
hence a * c divides b * d by A2, INT_2:16; :: thesis: verum