theorem Th9: :: NUMBER04:9

for n being Nat
for i being Integer holds <*i*> mod n = <*(i mod n)*>