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 l being Integer such that
A1: b = a * l ;
(a * l) * c = a * (l * c) ;
hence a divides b * c by A1; :: thesis: verum