theorem Th7: :: EULER_2:7

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