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 ();
((Sum (u (#) the CR_coefficients of m)) mod ()) mod () = (Sum (u (#) the CR_coefficients of m)) mod () by NAT_D:65;
then A3: (Sum (u (#) the CR_coefficients of m)) mod (), Sum (u (#) the CR_coefficients of m) are_congruent_mod Product m by NAT_D:64;
A4: dom m = Seg (len u) by
.= dom u by FINSEQ_1:def 3 ;
then ex y being Integer st y * (m . i) = Product m by ;
then (Sum (u (#) the CR_coefficients of m)) mod (), Sum (u (#) the CR_coefficients of m) are_congruent_mod m . i by ;
then A5: ((Sum (u (#) the CR_coefficients of m)) mod ()) mod (m . i) = (Sum (u (#) the CR_coefficients of m)) mod (m . i) by NAT_D:64;
dom m = Seg (len u) by
.= dom u by FINSEQ_1:def 3 ;
then m . i in rng m by ;
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 (),u . i are_congruent_mod m . i by ;
hence z,u . i are_congruent_mod m . i by ; :: 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 ; :: thesis: verum