theorem :: EULER_2:8

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