for m, n, l being Nat holds (l * m) mod n = ((l mod n) * m) mod n by Th7;