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