let i, j, h be Nat; :: thesis: ( i divides j implies i divides j * h )
assume i divides j ; :: thesis: i divides j * h
then consider l being Nat such that
A1: j = i * l by Def3;
(i * l) * h = i * (l * h) ;
hence i divides j * h by A1, Def3; :: thesis: verum