theorem Th27: :: INT_6:27

for m being CR_Sequence
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