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 A1, Lm2;
then to_int (((mod (u,m)) + (mod (v,m))),m) = (Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m) by Def5;
then (to_int (((mod (u,m)) + (mod (v,m))),m)) mod (Product m) = (Sum (((mod (u,m)) + (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m) 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 A3, INT_1:20;
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 A5, INT_1:15;
((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i by A4, Th33;
hence to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i by A6, INT_1:15; :: thesis: verum