let a, b, c be Integer; :: thesis: ( a divides b implies a divides b * c )
assume a divides b ; :: thesis: a divides b * c
then consider d being Integer such that
A1: b = a * d by INT_1:def 9;
b * c = a * (d * c) by A1;
hence a divides b * c by INT_1:def 9; :: thesis: verum