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 A1, Def3;
A4: len (mod (u,m)) = len m by Def3;
then len ((mod (u,m)) (#) (mod (v,m))) = len m by A2, Lm4;
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:def 4;
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, NAT_D:67;
m . i in rng m by A1, FUNCT_1:3;
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, NAT_D:64; :: thesis: verum