let n be non empty Nat; :: thesis: for i being Integer holds (i * n) mod n = 0
let i be Integer; :: thesis: (i * n) mod n = 0
(i * n) mod n = ((i mod n) * (n mod n)) mod n by INT_3:15
.= ((i mod n) * 0 ) mod n by NAT_D:25
.= 0 mod n ;
hence (i * n) mod n = 0 by NAT_D:26; :: thesis: verum