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 AS: i in dom m ; :: thesis: ((mod u,m) (#) (mod v,m)) . i,u * v are_congruent_mod m . i
C: len (mod v,m) = len m by Df1;
then CC: ( len (mod u,m) = len (mod v,m) & len (mod u,m) = len m ) by Df1;
then len ((mod u,m) (#) (mod v,m)) = len m by length3;
then A1: dom ((mod u,m) (#) (mod v,m)) = Seg (len m) by FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3 ;
m . i in rng m by AS, FUNCT_1:12;
then D1: m . i > 0 by PARTFUN3:def 1;
B1: ((mod u,m) (#) (mod v,m)) . i = ((mod u,m) . i) * ((mod v,m) . i) by A1, AS, VALUED_1:def 4;
D: dom (mod u,m) = Seg (len m) by CC, FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3 ;
dom (mod v,m) = Seg (len m) by C, FINSEQ_1:def 3
.= dom m by FINSEQ_1:def 3 ;
then ( (mod u,m) . i = u mod (m . i) & (mod v,m) . i = v mod (m . i) ) by D, AS, Df1;
then (((mod u,m) . i) * ((mod v,m) . i)) mod (m . i) = (u * v) mod (m . i) by INT_3:15;
hence ((mod u,m) (#) (mod v,m)) . i,u * v are_congruent_mod m . i by D1, B1, INT_3:12; :: thesis: verum