for i1, i2, i3 being Integer
for k being Nat st i1,i2 are_congruent_mod i3 holds
i1 * k,i2 * k are_congruent_mod i3 * k