let u, v be Integer; :: thesis: for m being CR_Sequence
for i being Nat 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 Nat st i in dom m holds
((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i

let i be Nat; :: 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 ;
A4: len (mod (u,m)) = len m by Def3;
then len ((mod (u,m)) (#) (mod (v,m))) = len m by ;
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 ;
dom (mod (u,m)) = Seg (len m) by
.= dom m by FINSEQ_1:def 3 ;
then (mod (u,m)) . i = u mod (m . i) by ;
then A6: (((mod (u,m)) . i) * ((mod (v,m)) . i)) mod (m . i) = (u * v) mod (m . i) by ;
m . i in rng m by ;
then m . i > 0 by PARTFUN3:def 1;
hence ((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i by ; :: thesis: verum