let m, n, l be Nat; :: thesis: (l * m) mod n = ((l mod n) * (m mod n)) mod n
(l * m) mod n = (l * (m mod n)) mod n by Th7;
hence (l * m) mod n = ((l mod n) * (m mod n)) mod n by Th7; :: thesis: verum