let i1, i2, i3, i be Integer; :: thesis: ( i1,i2 are_congruent_mod i implies i1 * i3,i2 * i3 are_congruent_mod i )
assume i1,i2 are_congruent_mod i ; :: thesis: i1 * i3,i2 * i3 are_congruent_mod i
then i divides i1 - i2 ;
then i divides (i1 - i2) * i3 by INT_2:2;
then i divides (i1 * i3) - (i2 * i3) ;
hence i1 * i3,i2 * i3 are_congruent_mod i ; :: thesis: verum