theorem Th3: :: RADIX_2:3

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