let i1, i2, i3, i be Integer; :: thesis: ( i1 * i,i2 * i are_congruent_mod i3 & i,i3 are_coprime implies i1,i2 are_congruent_mod i3 )
assume that
A1: i1 * i,i2 * i are_congruent_mod i3 and
A2: i,i3 are_coprime ; :: thesis: i1,i2 are_congruent_mod i3
i3 divides (i1 * i) - (i2 * i) by A1;
then i3 divides (i1 - i2) * i ;
then i3 divides i1 - i2 by A2, INT_2:25;
hence i1,i2 are_congruent_mod i3 ; :: thesis: verum