for m being Integer
for f, fr being FinSequence of INT st len f = len fr & ( for d being Nat st d in dom f holds
f . d,fr . d are_congruent_mod m ) holds
Product f, Product fr are_congruent_mod m