let u be INT -valued 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 Nat 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 Nat 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 Nat 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 Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) )

now :: thesis: for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i

set c = the CR_coefficients of m;
let i be Nat; :: 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 (#) the CR_coefficients of m)) mod (Product m);
((Sum (u (#) the CR_coefficients of m)) mod (Product m)) mod (Product m) = (Sum (u (#) the CR_coefficients of m)) mod (Product m) by NAT_D:65;
then A3: (Sum (u (#) the CR_coefficients of m)) mod (Product m), Sum (u (#) the CR_coefficients of m) are_congruent_mod Product m by NAT_D:64;
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 (#) the CR_coefficients of m)) mod (Product m), Sum (u (#) the CR_coefficients of m) are_congruent_mod m . i by A3, INT_1:20;
then A5: ((Sum (u (#) the CR_coefficients of m)) mod (Product m)) mod (m . i) = (Sum (u (#) the CR_coefficients of m)) mod (m . i) by NAT_D:64;
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:3;
then A6: m . i > 0 by PARTFUN3:def 1;
Sum (u (#) the CR_coefficients of m),u . i are_congruent_mod m . i by A1, A2, A4, Th29;
then (Sum (u (#) the CR_coefficients of m)) mod (m . i) = (u . i) mod (m . i) by NAT_D:64;
then (Sum (u (#) the CR_coefficients of m)) mod (Product m),u . i are_congruent_mod m . i by A6, A5, NAT_D:64;
hence z,u . i are_congruent_mod m . i by A1, Def5; :: thesis: verum

end;

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