let u be integer-yielding FinSequence; :: thesis: for m being CR_Sequence st len u = len m holds
ex z being Integer st
( 0 <= z & z < Product m & ( for i being natural number st i in dom u holds
z,u . i are_congruent_mod m . i ) )
let m be CR_Sequence; :: thesis: ( len u = len m implies ex z being Integer st
( 0 <= z & z < Product m & ( for i being natural number st i in dom u holds
z,u . i are_congruent_mod m . i ) ) )
assume A1: len u = len m ; :: thesis: ex z being Integer st
( 0 <= z & z < Product m & ( for i being natural number st i in dom u holds
z,u . i are_congruent_mod m . i ) )
take z = to_int u,m; :: thesis: ( 0 <= z & z < Product m & ( for i being natural number st i in dom u holds
z,u . i are_congruent_mod m . i ) )

now

consider c being CR_coefficients of m;
let i be natural number ; :: thesis: ( i in dom u implies z,u . i are_congruent_mod m . i )
assume A2: i in dom u ; :: thesis: z,u . i are_congruent_mod m . i
set s = (Sum (u (#) c)) mod (Product m);
((Sum (u (#) c)) mod (Product m)) mod (Product m) = (Sum (u (#) c)) mod (Product m) by INT_3:13;
then A3: (Sum (u (#) c)) mod (Product m), Sum (u (#) c) are_congruent_mod Product m by INT_3:12;
A4: dom m = Seg (len u) by A1, FINSEQ_1:def 3
.= dom u by FINSEQ_1:def 3 ;
then ex y being Integer st y * (m . i) = Product m by A2, Th10;
then (Sum (u (#) c)) mod (Product m), Sum (u (#) c) are_congruent_mod m . i by A3, INT_1:41;
then A5: ((Sum (u (#) c)) mod (Product m)) mod (m . i) = (Sum (u (#) c)) mod (m . i) by INT_3:12;
dom m = Seg (len u) by A1, FINSEQ_1:def 3
.= dom u by FINSEQ_1:def 3 ;
then m . i in rng m by A2, FUNCT_1:12;
then A6: m . i > 0 by PARTFUN3:def 1;
Sum (u (#) c),u . i are_congruent_mod m . i by A1, A2, A4, Th29;
then (Sum (u (#) c)) mod (m . i) = (u . i) mod (m . i) by INT_3:12;
then (Sum (u (#) c)) mod (Product m),u . i are_congruent_mod m . i by A6, A5, INT_3:12;
hence z,u . i are_congruent_mod m . i by A1, Def5; :: thesis: verum

end;

hence ( 0 <= z & z < Product m & ( for i being natural number st i in dom u holds
z,u . i are_congruent_mod m . i ) ) by A1, Th31; :: thesis: verum