theorem :: EULER_2:14

for a, m being Nat
for F being FinSequence of NAT holds (a * (F mod m)) mod m = (a * F) mod m