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 ();
set s2 = (Sum (u (#) c2)) mod ();
A2: (Sum (u (#) c1)) mod () < Product m by NAT_D:62;
A3: for i being Nat st i in dom m holds
(Sum (u (#) c1)) mod (),u . i are_congruent_mod m . i
proof
let i be Nat; :: thesis: ( i in dom m implies (Sum (u (#) c1)) mod (),u . i are_congruent_mod m . i )
((Sum (u (#) c1)) mod ()) mod () = (Sum (u (#) c1)) mod () by NAT_D:65;
then A4: (Sum (u (#) c1)) mod (), Sum (u (#) c1) are_congruent_mod Product m by NAT_D:64;
assume A5: i in dom m ; :: thesis: (Sum (u (#) c1)) mod (),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 ;
then (Sum (u (#) c1)) mod (), Sum (u (#) c1) are_congruent_mod m . i by ;
then A7: ((Sum (u (#) c1)) mod ()) 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 (),u . i are_congruent_mod m . i by ; :: thesis: verum
end;
A8: 0 <= (Sum (u (#) c2)) mod () by NAT_D:62;
A9: for i being Nat st i in dom m holds
(Sum (u (#) c2)) mod (),u . i are_congruent_mod m . i
proof
let i be Nat; :: thesis: ( i in dom m implies (Sum (u (#) c2)) mod (),u . i are_congruent_mod m . i )
((Sum (u (#) c2)) mod ()) mod () = (Sum (u (#) c2)) mod () by NAT_D:65;
then A10: (Sum (u (#) c2)) mod (), Sum (u (#) c2) are_congruent_mod Product m by NAT_D:64;
assume A11: i in dom m ; :: thesis: (Sum (u (#) c2)) mod (),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 ;
then (Sum (u (#) c2)) mod (), Sum (u (#) c2) are_congruent_mod m . i by ;
then A13: ((Sum (u (#) c2)) mod ()) mod (m . i) = (Sum (u (#) c2)) mod (m . i) by NAT_D:64;
Sum (u (#) c2),u . i are_congruent_mod m . i by ;
then (Sum (u (#) c2)) mod (m . i) = (u . i) mod (m . i) by NAT_D:64;
hence (Sum (u (#) c2)) mod (),u . i are_congruent_mod m . i by ; :: thesis: verum
end;
A14: (Sum (u (#) c2)) mod () < Product m by NAT_D:62;
0 <= (Sum (u (#) c1)) mod () by NAT_D:62;
then (Sum (u (#) c1)) mod () = (Sum (u (#) c2)) mod () 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