theorem Th11: :: NTALGO_1:11

for nlist being non empty FinSequence of [:INT,INT:]
for a, b being FinSequence of INT st len a = len b & len a = len nlist & ( for i being Nat st i in Seg (len nlist) holds
b . i <> 0 ) & ( for i being Nat st i in Seg (len nlist) holds
( (nlist . i) `1 = a . i & (nlist . i) `2 = b . i ) ) & ( for i, j being Nat st i in Seg (len nlist) & j in Seg (len nlist) & i <> j holds
b . i,b . j are_coprime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i)