for m being CR_Sequence
for j being Nat
for x being Integer st j in dom m holds
(x mod (Product m)) mod (m . j) = x mod (m . j)