theorem :: NUMBER19:6

for u being integer-valued FinSequence
for m being CR_Sequence st dom u = dom m holds
for z being Nat st z solves_CRT u,m & ( for i being Nat st i in dom u holds
u . i,m . i are_coprime ) holds
z, Product m are_coprime