theorem Th2: :: RADIX_2:2

for a, b being Integer
for n being Nat holds ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n