theorem Th30: :: NUMBER14:30

for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
for z being Integer st z solves_CRT u,m holds
for k being Integer holds z + (k * (Product m)) solves_CRT u,m