for m being Nat
for f being FinSequence of NAT st m <> 0 holds
(Product (f mod m)) mod m = (Product f) mod m