let n be Nat; :: thesis: for i being Integer holds i * n,n are_congruent_mod n
let i be Integer; :: thesis: i * n,n are_congruent_mod n
A1: i * n, 0 are_congruent_mod n ;
0 ,n are_congruent_mod n by INT_1:12;
hence i * n,n are_congruent_mod n by A1, INT_1:15; :: thesis: verum