let u, v be Integer; :: thesis: for m being CR_Sequence
for i being Nat st i in dom m holds
to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i

let m be CR_Sequence; :: thesis: for i being Nat st i in dom m holds
to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i

let i be Nat; :: thesis: ( i in dom m implies to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i )
set z = to_int (((mod (u,m)) + (mod (v,m))),m);
set c = the CR_coefficients of m;
A1: len (mod (u,m)) = len m by Def3;
len (mod (v,m)) = len m by Def3;
then A2: len ((mod (u,m)) + (mod (v,m))) = len m by ;
then to_int (((mod (u,m)) + (mod (v,m))),m) = (Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m)) mod () by Def5;
then (to_int (((mod (u,m)) + (mod (v,m))),m)) mod () = (Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m)) mod () by NAT_D:65;
then A3: to_int (((mod (u,m)) + (mod (v,m))),m), Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod Product m by NAT_D:64;
assume A4: i in dom m ; :: thesis: to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i
then ex y being Integer st y * (m . i) = Product m by Th10;
then A5: to_int (((mod (u,m)) + (mod (v,m))),m), Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod m . i by ;
Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m),((mod (u,m)) + (mod (v,m))) . i are_congruent_mod m . i by A4, A2, Th29;
then A6: to_int (((mod (u,m)) + (mod (v,m))),m),((mod (u,m)) + (mod (v,m))) . i are_congruent_mod m . i by ;
((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i by ;
hence to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i by ; :: thesis: verum