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,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m