theorem Th12: :: EULER_1:12

for i, k, n being Integer holds (i + (k * n)) mod n = i mod n