let m be CR_Sequence; :: thesis: for c1, c2 being CR_coefficients of m
for i being Nat 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 Nat st i in dom c1 holds
c1 . i,c2 . i are_congruent_mod m . i
let i be Nat; :: thesis: ( i in dom c1 implies c1 . i,c2 . i are_congruent_mod m . i )
assume A1: i in dom c1 ; :: thesis: c1 . i,c2 . i are_congruent_mod m . i
then A2: ex s1, mm1 being Integer st
( mm1 = (Product m) / (m . i) & s1 * mm1,1 are_congruent_mod m . i & c1 . i = s1 * ((Product m) / (m . i)) ) by Def4;
A3: len c1 = len m by Def4
.= len c2 by Def4 ;
dom c1 = Seg (len c1) by FINSEQ_1:def 3
.= dom c2 by A3, FINSEQ_1:def 3 ;
then consider s2, mm2 being Integer such that
A4: mm2 = (Product m) / (m . i) and
A5: s2 * mm2,1 are_congruent_mod m . i and
A6: c2 . i = s2 * ((Product m) / (m . i)) by A1, Def4;
1,s2 * mm2 are_congruent_mod m . i by A5, INT_1:14;
hence c1 . i,c2 . i are_congruent_mod m . i by A2, A4, A6, INT_1:15; :: thesis: verum