let l, m, n 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 Th9;
hence (l * m) mod n = ((l mod n) * (m mod n)) mod n by Th9; :: thesis: verum