let i, j, k be Integer; :: thesis: ( i divides j implies k * i divides k * j )
assume i divides j ; :: thesis: k * i divides k * j
then consider z being Integer such that
A1: i * z = j by INT_1:def 3;
(i * k) * z = j * k by A1;
hence k * i divides k * j by INT_1:def 3; :: thesis: verum