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