let m be CR_Sequence; :: thesis: for c being CR_coefficients of m
for i being natural number 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 natural number st i in dom c holds
c . i,1 are_congruent_mod m . i
let i be natural number ; :: 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 consider s, mm being Integer such that
A: ( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & c . i = s * ((Product m) / (m . i)) ) by defCi;
thus c . i,1 are_congruent_mod m . i by A; :: thesis: verum