theorem Th20: :: BINARI_4:20

for n being non zero Nat
for i being Integer holds (i * n) mod n = 0 ;