let m be CR_Sequence; :: thesis: for c being CR_coefficients of m
for i being Nat st i in dom c holds
c . i,1 are_congruent_mod m . i
let c be CR_coefficients of m; :: thesis: for i being Nat st i in dom c holds
c . i,1 are_congruent_mod m . i
let i be Nat; :: thesis: ( i in dom c implies c . i,1 are_congruent_mod m . i )
assume i in dom c ; :: thesis: c . i,1 are_congruent_mod m . i
then ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & c . i = s * ((Product m) / (m . i)) ) by Def4;
hence c . i,1 are_congruent_mod m . i ; :: thesis: verum