let m be CR_Sequence; :: thesis: for c being CR_coefficients of m

for i, j being Nat 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 Nat st i in dom c & j in dom c & i <> j holds

c . i, 0 are_congruent_mod m . j

let i, j be Nat; :: thesis: ( i in dom c & j in dom c & i <> j implies c . i, 0 are_congruent_mod m . j )

assume that

A1: i in dom c and

A2: j in dom c and

A3: i <> j ; :: thesis: c . i, 0 are_congruent_mod m . j

consider s, mm being Integer such that

A4: mm = (Product m) / (m . i) and

s * mm,1 are_congruent_mod m . i and

A5: c . i = s * ((Product m) / (m . i)) by A1, Def4;

len m = len c by Def4;

then dom m = Seg (len c) by FINSEQ_1:def 3

.= dom c by FINSEQ_1:def 3 ;

then consider z being Integer such that

A6: z * (m . j) = mm by A1, A2, A3, A4, Lm6;

A7: m . j, 0 are_congruent_mod m . j by INT_1:12;

A8: s,s are_congruent_mod m . j by INT_1:11;

z,z are_congruent_mod m . j by INT_1:11;

then z * (m . j),z * 0 are_congruent_mod m . j by A7, INT_1:18;

then s * mm,s * 0 are_congruent_mod m . j by A6, A8, INT_1:18;

hence c . i, 0 are_congruent_mod m . j by A4, A5; :: thesis: verum

for i, j being Nat 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 Nat st i in dom c & j in dom c & i <> j holds

c . i, 0 are_congruent_mod m . j

let i, j be Nat; :: thesis: ( i in dom c & j in dom c & i <> j implies c . i, 0 are_congruent_mod m . j )

assume that

A1: i in dom c and

A2: j in dom c and

A3: i <> j ; :: thesis: c . i, 0 are_congruent_mod m . j

consider s, mm being Integer such that

A4: mm = (Product m) / (m . i) and

s * mm,1 are_congruent_mod m . i and

A5: c . i = s * ((Product m) / (m . i)) by A1, Def4;

len m = len c by Def4;

then dom m = Seg (len c) by FINSEQ_1:def 3

.= dom c by FINSEQ_1:def 3 ;

then consider z being Integer such that

A6: z * (m . j) = mm by A1, A2, A3, A4, Lm6;

A7: m . j, 0 are_congruent_mod m . j by INT_1:12;

A8: s,s are_congruent_mod m . j by INT_1:11;

z,z are_congruent_mod m . j by INT_1:11;

then z * (m . j),z * 0 are_congruent_mod m . j by A7, INT_1:18;

then s * mm,s * 0 are_congruent_mod m . j by A6, A8, INT_1:18;

hence c . i, 0 are_congruent_mod m . j by A4, A5; :: thesis: verum