let m be CR_Sequence; :: thesis: for c being CR_coefficients of m
for i, j being natural number st i in dom c & j in dom c & i <> j holds
c . i, 0 are_congruent_mod m . j
let c be CR_coefficients of m; :: thesis: for i, j being natural number st i in dom c & j in dom c & i <> j holds
c . i, 0 are_congruent_mod m . j
let i, j be natural number ; :: thesis: ( i in dom c & j in dom c & i <> j implies c . i, 0 are_congruent_mod m . j )
assume AS: ( i in dom c & j in dom c & i <> j ) ; :: thesis: c . i, 0 are_congruent_mod m . j
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;
len m = len c by defCi;
then D: dom m = Seg (len c) by FINSEQ_1:def 3
.= dom c by FINSEQ_1:def 3 ;
consider z being Integer such that
C: z * (m . j) = mm by AS, A, x0000, D;
B1: s,s are_congruent_mod m . j by INT_1:32;
B2: z,z are_congruent_mod m . j by INT_1:32;
m . j, 0 are_congruent_mod m . j by INT_1:33;
then z * (m . j),z * 0 are_congruent_mod m . j by B2, INT_1:39;
then s * mm,s * 0 are_congruent_mod m . j by C, B1, INT_1:39;
hence c . i, 0 are_congruent_mod m . j by A; :: thesis: verum