let u be INT -valued 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 A1: 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);
A2: (Sum (u (#) c1)) mod (Product m) < Product m by NAT_D:62;
A3: for i being Nat st i in dom m holds
(Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i

proof

let i be Nat; :: thesis: ( i in dom m implies (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i )
((Sum (u (#) c1)) mod (Product m)) mod (Product m) = (Sum (u (#) c1)) mod (Product m) by NAT_D:65;
then A4: (Sum (u (#) c1)) mod (Product m), Sum (u (#) c1) are_congruent_mod Product m by NAT_D:64;
assume A5: i in dom m ; :: thesis: (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i
then m . i in rng m by FUNCT_1:3;
then A6: m . i > 0 by PARTFUN3:def 1;
ex z being Integer st z * (m . i) = Product m by A5, Th10;
then (Sum (u (#) c1)) mod (Product m), Sum (u (#) c1) are_congruent_mod m . i by A4, INT_1:20;
then A7: ((Sum (u (#) c1)) mod (Product m)) mod (m . i) = (Sum (u (#) c1)) mod (m . i) by NAT_D:64;
Sum (u (#) c1),u . i are_congruent_mod m . i by A1, A5, Th29;
then (Sum (u (#) c1)) mod (m . i) = (u . i) mod (m . i) by NAT_D:64;
hence (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i by A6, A7, NAT_D:64; :: thesis: verum

end;

A8: 0 <= (Sum (u (#) c2)) mod (Product m) by NAT_D:62;
A9: for i being Nat st i in dom m holds
(Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i

proof

let i be Nat; :: thesis: ( i in dom m implies (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i )
((Sum (u (#) c2)) mod (Product m)) mod (Product m) = (Sum (u (#) c2)) mod (Product m) by NAT_D:65;
then A10: (Sum (u (#) c2)) mod (Product m), Sum (u (#) c2) are_congruent_mod Product m by NAT_D:64;
assume A11: i in dom m ; :: thesis: (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i
then m . i in rng m by FUNCT_1:3;
then A12: m . i > 0 by PARTFUN3:def 1;
ex z being Integer st z * (m . i) = Product m by A11, Th10;
then (Sum (u (#) c2)) mod (Product m), Sum (u (#) c2) are_congruent_mod m . i by A10, INT_1:20;
then A13: ((Sum (u (#) c2)) mod (Product m)) mod (m . i) = (Sum (u (#) c2)) mod (m . i) by NAT_D:64;
Sum (u (#) c2),u . i are_congruent_mod m . i by A1, A11, Th29;
then (Sum (u (#) c2)) mod (m . i) = (u . i) mod (m . i) by NAT_D:64;
hence (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i by A12, A13, NAT_D:64; :: thesis: verum

end;

A14: (Sum (u (#) c2)) mod (Product m) < Product m by NAT_D:62;
0 <= (Sum (u (#) c1)) mod (Product m) by NAT_D:62;
then (Sum (u (#) c1)) mod (Product m) = (Sum (u (#) c2)) mod (Product m) by A3, A9, A2, A8, A14, Lm9;
hence Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m by NAT_D:64; :: thesis: verum