theorem Th5: :: NUMBER19:5

for u being integer-valued FinSequence
for m being CR_Sequence
for z being Integer st z solves_CRT u,m holds
for i being Nat st i in dom u & u . i,m . i are_coprime holds
z,m . i are_coprime by NUMBER14:def 3, WSIERP_1:43;