let u, v be Integer; :: thesis: for m being CR_Sequence
for i being natural number st i in dom m holds
((mod u,m) - (mod v,m)) . i,u - v are_congruent_mod m . i
let m be CR_Sequence; :: thesis: for i being natural number st i in dom m holds
((mod u,m) - (mod v,m)) . i,u - v are_congruent_mod m . i
let i be natural number ; :: thesis: ( i in dom m implies ((mod u,m) - (mod v,m)) . i,u - v are_congruent_mod m . i )
assume A1: i in dom m ; :: thesis: ((mod u,m) - (mod v,m)) . i,u - v are_congruent_mod m . i
A2: len (mod v,m) = len m by Def3;
then dom (mod v,m) = Seg (len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3 ;
then A3: (mod v,m) . i = v mod (m . i) by A1, Def3;
A4: len (mod u,m) = len m by Def3;
then len ((mod u,m) - (mod v,m)) = len m by A2, Lm3;
then dom ((mod u,m) - (mod v,m)) = Seg (len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3 ;
then A5: ((mod u,m) - (mod v,m)) . i = ((mod u,m) . i) - ((mod v,m) . i) by A1, VALUED_1:13;
dom (mod u,m) = Seg (len m) by A4, FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3 ;
then (mod u,m) . i = u mod (m . i) by A1, Def3;
then A6: (((mod u,m) . i) - ((mod v,m) . i)) mod (m . i) = (u - v) mod (m . i) by A3, Th7;
m . i in rng m by A1, FUNCT_1:12;
then m . i > 0 by PARTFUN3:def 1;
hence ((mod u,m) - (mod v,m)) . i,u - v are_congruent_mod m . i by A5, A6, INT_3:12; :: thesis: verum