theorem Th3: :: RADIX_1:3

for k, m, n being Nat st m <> 0 holds
(k mod (m * n)) mod n = k mod n