let i1, i2, i3 be Integer; :: thesis: for k being Nat st i1,i2 are_congruent_mod i3 holds
i1 * k,i2 * k are_congruent_mod i3 * k
let k be Nat; :: thesis: ( i1,i2 are_congruent_mod i3 implies i1 * k,i2 * k are_congruent_mod i3 * k )
assume i1,i2 are_congruent_mod i3 ; :: thesis: i1 * k,i2 * k are_congruent_mod i3 * k
then consider i4 being Integer such that
A1: i3 * i4 = i1 - i2 ;
(i3 * k) * i4 = (i3 * i4) * k
.= (i1 + (- i2)) * k by A1
.= (i1 * k) - (i2 * k) ;
hence i1 * k,i2 * k are_congruent_mod i3 * k ; :: thesis: verum