theorem :: INT_6:42

for u being INT -valued FinSequence
for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2 by Lm9;