theorem :: EULER_2:11

for m being Nat
for f being integer-valued FinSequence st m <> 0 holds
(Product (f mod m)) mod m = (Product f) mod m