let u, v be Integer; 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; 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; ( 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
; ((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; verum