let i1, i2, i, i3 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 by INT_2:15;
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 by INT_2:15; :: thesis: verum