theorem :: EULER_2:8

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