let u, v be Integer; :: thesis: for m being CR_Sequence
for i being natural number 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 natural number 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 natural number ; :: 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;
consider c being 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)) (#) c)) 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)) (#) c)) mod (Product m) by INT_3:13;
then A3: to_int ((mod u,m) + (mod v,m)),m, Sum (((mod u,m) + (mod v,m)) (#) c) are_congruent_mod Product m by INT_3:12;
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)) (#) c) are_congruent_mod m . i by A3, INT_1:41;
Sum (((mod u,m) + (mod v,m)) (#) c),((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:36;
((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:36; :: thesis: verum