let i be Integer; :: thesis: for n being Nat holds (i * n) mod n = 0
let n be Nat; :: thesis: (i * n) mod n = 0
(i * n) mod n = ((i mod n) * (n mod n)) mod n by Th67
.= ((i mod n) * 0) mod n by Th25
.= 0 mod n ;
hence (i * n) mod n = 0 by Th26; :: thesis: verum