let u be integer-yielding FinSequence; :: thesis: 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
let m be CR_Sequence; :: thesis: ( len m = len u implies for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m )
assume H0: len u = len m ; :: thesis: for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
let c1, c2 be CR_coefficients of m; :: thesis: Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
set s1 = (Sum (u (#) c1)) mod (Product m);
set s2 = (Sum (u (#) c2)) mod (Product m);
A: for i being natural number st i in dom m holds
(Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i

proof

let i be natural number ; :: thesis: ( i in dom m implies (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i )
assume A0: i in dom m ; :: thesis: (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i
then Sum (u (#) c1),u . i are_congruent_mod m . i by H0, congsum;
then C: (Sum (u (#) c1)) mod (m . i) = (u . i) mod (m . i) by INT_3:12;
m . i in rng m by A0, FUNCT_1:12;
then D1: m . i > 0 by PARTFUN3:def 1;
consider z being Integer such that
E: z * (m . i) = Product m by A0, x000;
((Sum (u (#) c1)) mod (Product m)) mod (Product m) = (Sum (u (#) c1)) mod (Product m) by INT_3:13;
then (Sum (u (#) c1)) mod (Product m), Sum (u (#) c1) are_congruent_mod Product m by INT_3:12;
then (Sum (u (#) c1)) mod (Product m), Sum (u (#) c1) are_congruent_mod m . i by E, INT_1:41;
then ((Sum (u (#) c1)) mod (Product m)) mod (m . i) = (Sum (u (#) c1)) mod (m . i) by INT_3:12;
hence (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i by D1, C, INT_3:12; :: thesis: verum

end;

B: for i being natural number st i in dom m holds
(Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i

proof

let i be natural number ; :: thesis: ( i in dom m implies (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i )
assume A0: i in dom m ; :: thesis: (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i
then Sum (u (#) c2),u . i are_congruent_mod m . i by H0, congsum;
then C: (Sum (u (#) c2)) mod (m . i) = (u . i) mod (m . i) by INT_3:12;
m . i in rng m by A0, FUNCT_1:12;
then D1: m . i > 0 by PARTFUN3:def 1;
consider z being Integer such that
E: z * (m . i) = Product m by A0, x000;
((Sum (u (#) c2)) mod (Product m)) mod (Product m) = (Sum (u (#) c2)) mod (Product m) by INT_3:13;
then (Sum (u (#) c2)) mod (Product m), Sum (u (#) c2) are_congruent_mod Product m by INT_3:12;
then (Sum (u (#) c2)) mod (Product m), Sum (u (#) c2) are_congruent_mod m . i by E, INT_1:41;
then ((Sum (u (#) c2)) mod (Product m)) mod (m . i) = (Sum (u (#) c2)) mod (m . i) by INT_3:12;
hence (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i by D1, C, INT_3:12; :: thesis: verum

end;

C: ( 0 <= (Sum (u (#) c1)) mod (Product m) & (Sum (u (#) c1)) mod (Product m) < Product m ) by INT_3:9;
( 0 <= (Sum (u (#) c2)) mod (Product m) & (Sum (u (#) c2)) mod (Product m) < Product m ) by INT_3:9;
then (Sum (u (#) c1)) mod (Product m) = (Sum (u (#) c2)) mod (Product m) by A, B, C, Th3;
hence Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m by INT_3:12; :: thesis: verum