for u being INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m