let m be CR_Sequence; :: thesis: for c1, c2 being CR_coefficients of m
for i being natural number st i in dom c1 holds
c1 . i,c2 . i are_congruent_mod m . i
let c1, c2 be CR_coefficients of m; :: thesis: for i being natural number st i in dom c1 holds
c1 . i,c2 . i are_congruent_mod m . i
let i be natural number ; :: thesis: ( i in dom c1 implies c1 . i,c2 . i are_congruent_mod m . i )
assume AS: i in dom c1 ; :: thesis: c1 . i,c2 . i are_congruent_mod m . i
then consider s1, mm1 being Integer such that
A1: ( mm1 = (Product m) / (m . i) & s1 * mm1,1 are_congruent_mod m . i & c1 . i = s1 * ((Product m) / (m . i)) ) by defCi;
H1: len c1 = len m by defCi
.= len c2 by defCi ;
dom c1 = Seg (len c1) by FINSEQ_1:def 3
.= dom c2 by H1, FINSEQ_1:def 3 ;
then consider s2, mm2 being Integer such that
A2: ( mm2 = (Product m) / (m . i) & s2 * mm2,1 are_congruent_mod m . i & c2 . i = s2 * ((Product m) / (m . i)) ) by AS, defCi;
1,s2 * mm2 are_congruent_mod m . i by A2, INT_1:35;
hence c1 . i,c2 . i are_congruent_mod m . i by A1, A2, INT_1:36; :: thesis: verum