defpred S₁[ Nat] means for nlist being non empty FinSequence of [:INT,INT:]
for a, b being FinSequence of INT st len nlist = $1 & 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_relative_prime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i);
P0: S₁[ 0 ] ;
P1: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

let n be Element of NAT ; :: thesis:
assume AS1: S₁[n] ; :: thesis:
let nlist be non empty FinSequence of [:INT,INT:]; :: thesis:
let a, b be FinSequence of INT ; :: thesis:
assume AS2: ( len nlist = n + 1 & 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_relative_prime ) ) ; :: thesis:

suppose P1: n = 0 ; :: thesis:

P2: 1 in Seg (len nlist) by P1, AS2;
P3: ALGO_CRT nlist = (nlist . 1) `1 by defALGOCRT, P1, AS2
.= a . 1 by AS2, P2 ;
thus for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by P3, TARSKI:def 1, FINSEQ_1:2, P1, AS2; :: thesis:

end;

suppose NN1: n <> 0 ; :: thesis:

then NN2: 1 <= n by NAT_1:14;
P4: len nlist <> 1 by AS2, NN1;
reconsider nlist1 = nlist | n as FinSequence of [:INT,INT:] ;
reconsider a1 = a | n as FinSequence of INT ;
reconsider b1 = b | n as FinSequence of INT ;
KK: n <= n + 1 by NAT_1:11;
then D02: len a1 = n by FINSEQ_1:59, AS2;
D22: len nlist1 = n by KK, FINSEQ_1:59, AS2;
then reconsider nlist1 = nlist1 as non empty FinSequence of [:INT,INT:] by NN1;
D23: dom nlist1 = Seg (len nlist1) by FINSEQ_1:def 3
.= Seg n by KK, FINSEQ_1:59, AS2 ;
D25: len nlist1 = n by D23, FINSEQ_1:def 3;
then D28: Seg (len nlist1) c= Seg (len nlist) by KK, FINSEQ_1:5, AS2;
X1: ( len nlist1 = n & len a1 = len b1 & len a1 = len nlist1 ) by D02, KK, FINSEQ_1:59, AS2;
X2A: for i being Nat st i in Seg (len nlist1) holds
b1 . i <> 0

proof

let i be Nat; :: thesis:
assume D260: i in Seg (len nlist1) ; :: thesis:
then b1 . i = b . i by FUNCT_1:49, D25;
hence b1 . i <> 0 by D28, D260, AS2; :: thesis:

end;

X2: for i being Nat st i in Seg (len nlist1) holds
( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i )

proof

let i be Nat; :: thesis:
assume X21: i in Seg (len nlist1) ; :: thesis:
X23: (nlist1 . i) `1 = (nlist . i) `1 by X21, FUNCT_1:49, D25
.= a . i by X21, D28, AS2
.= a1 . i by X21, FUNCT_1:49, D25 ;
(nlist1 . i) `2 = (nlist . i) `2 by X21, FUNCT_1:49, D25
.= b . i by X21, D28, AS2
.= b1 . i by X21, FUNCT_1:49, D25 ;
hence ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) by X23; :: thesis:

end;

X3: for i, j being Nat st i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j holds
b1 . i,b1 . j are_relative_prime

proof

let i, j be Nat; :: thesis:
assume A1: ( i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j ) ; :: thesis:
A3: b . i = b1 . i by A1, FUNCT_1:49, D25;
b . j = b1 . j by A1, FUNCT_1:49, D25;
hence b1 . i,b1 . j are_relative_prime by A3, A1, D28, AS2; :: thesis:

end;

X400: for i being Nat st i in Seg (len nlist1) holds
(ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i)

proof

let i be Nat; :: thesis:
assume A1: i in Seg (len nlist1) ; :: thesis:
then ( a1 . i = a . i & b1 . i = b . i ) by FUNCT_1:49, D25;
hence (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) by AS1, X1, X2, X3, X2A, A1; :: thesis:

end;

consider m, l, prodc, prodi being FinSequence of INT , M0, M being Element of INT such that
X5: ( len m = len nlist & len l = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & l . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (l . i)) * (prodi . i)) mod u1 & l . (i + 1) = (l . i) + (u * (prodc . i)) ) ) & ALGO_CRT nlist = (l . (len m)) mod M ) by P4, defALGOCRT;
LmTh51: 1 + 1 <= n + 1 by XREAL_1:6, NN2;
reconsider lb1 = (len b) - 1 as Element of NAT by AS2;
LmTh54: ( 1 <= lb1 & lb1 <= lb1 ) by AS2, NAT_1:14, NN1;
LmTh55: for i being Nat st 1 <= i & i <= lb1 holds
m . (i + 1) = (m . i) * (b . i)

proof

let i be Nat; :: thesis:
assume PX0: ( 1 <= i & i <= lb1 ) ; :: thesis:
then PX1: ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) by AS2, X5;
i in Seg (len nlist1) by PX0, D22, AS2, FINSEQ_1:1;
hence m . (i + 1) = (m . i) * (b . i) by PX1, AS2, D28; :: thesis:

end;

LmTh56: m . (len nlist),b . (len nlist) are_relative_prime by AS2, LmTh5, LmTh51, X5, LmTh54, LmTh55;
set l1 = l | n;
set m1 = m | n;
KK: n <= n + 1 by NAT_1:11;
then PD02: len (l | n) = n by AS2, FINSEQ_1:59, X5;
PD11: dom (m | n) = Seg (len (m | n)) by FINSEQ_1:def 3
.= Seg n by AS2, FINSEQ_1:59, X5, KK ;
PD12: len (m | n) = n by PD11, FINSEQ_1:def 3;
1 - 1 <= n - 1 by NN2, XREAL_1:9;
then n - 1 in NAT by INT_1:3;
then reconsider nn1 = n - 1 as Nat ;
reconsider prodi1 = prodi | nn1 as FinSequence of INT ;
reconsider prodc1 = prodc | nn1 as FinSequence of INT ;
XX5: n - 1 <= n - 0 by XREAL_1:10;
then QD02: len prodi1 = nn1 by AS2, X5, FINSEQ_1:59;
QD12: len prodc1 = nn1 by XX5, AS2, X5, FINSEQ_1:59;
PD24: 1 in Seg n by NN2;
PD26X: (l | n) . 1 = l . 1 by FUNCT_1:49, PD24
.= (nlist1 . 1) `1 by FUNCT_1:49, PD24, X5 ;
QKK: n - 1 <= n - 0 by XREAL_1:10;

PD26: now :: thesis:

let i be Nat; :: thesis:
assume PD260X: ( 1 <= i & i <= (len (m | n)) - 1 ) ; :: thesis:
then PD260: ( 1 <= i & i <= len (m | n) ) by PD12, QKK, XXREAL_0:2;
then i in Seg (len (m | n)) by FINSEQ_1:1;
hence (m | n) . i = m . i by FUNCT_1:49, PD12; :: thesis:
i in Seg (len (l | n)) by FINSEQ_1:1, PD260, PD02, PD12;
hence (l | n) . i = l . i by FUNCT_1:49, PD02; :: thesis:
i in Seg (len prodi1) by FINSEQ_1:1, PD260X, PD12, QD02;
hence prodi1 . i = prodi . i by FUNCT_1:49, QD02; :: thesis:
i in Seg (len prodc1) by FINSEQ_1:1, PD260X, PD12, QD12;
hence prodc1 . i = prodc . i by FUNCT_1:49, QD12; :: thesis:

end;

len (m | n) in Seg (len nlist1) by D22, PD12, FINSEQ_1:3;
then Z1: len (m | n) in Seg (len nlist) by D28;
Z2: nlist1 . (len (m | n)) = nlist . (len (m | n)) by FUNCT_1:49, D22, PD12, FINSEQ_1:3;
len (m | n) in dom nlist by FINSEQ_1:def 3, Z1;
then nlist1 . (len (m | n)) in [:INT,INT:] by FINSEQ_2:11, Z2;
then reconsider M01 = (nlist1 . (len (m | n))) `2 as Element of INT by MCART_1:10;
reconsider M1 = (prodc1 . ((len (m | n)) - 1)) * M01 as Element of INT by INT_1:def 2;
QX1: ( len (m | n) = len nlist1 & len (l | n) = len nlist1 & len prodc1 = (len nlist1) - 1 & len prodi1 = (len nlist1) - 1 & (m | n) . 1 = 1 ) by KK, FINSEQ_1:59, AS2, PD12, PD02, QD12, QD02, X5, FUNCT_1:49, PD24;
QX2: for i being Nat st 1 <= i & i <= (len (m | n)) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y )

proof

let i be Nat; :: thesis:
assume XQ21: ( 1 <= i & i <= (len (m | n)) - 1 ) ; :: thesis:
then XQ22: (m | n) . i = m . i by PD26;
XQ23: prodi1 . i = prodi . i by PD26, XQ21;
XQ24: prodc1 . i = prodc . i by PD26, XQ21;
XQ25: 1 <= i + 1 by NAT_1:12;
i + 1 <= ((len (m | n)) - 1) + 1 by XQ21, XREAL_1:6;
then YY1: i + 1 in Seg (len (m | n)) by XQ25;
then XQ27: (m | n) . (i + 1) = m . (i + 1) by FUNCT_1:49, PD12;
XQ28: ( 1 <= i & i <= len (m | n) ) by XQ21, PD12, QKK, XXREAL_0:2;
XQ30: ( 1 <= i & i <= (len m) - 1 ) by X5, AS2, XQ21, PD12, QKK, XXREAL_0:2;
i in Seg (len nlist1) by PD12, D22, XQ28, FINSEQ_1:1;
then XQ32: nlist1 . i = nlist . i by FUNCT_1:49, D25;
nlist1 . (i + 1) = nlist . (i + 1) by FUNCT_1:49, PD12, YY1;
hence ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | n) . (i + 1) = ((m | n) . i) * x & y = (m | n) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by XQ22, XQ23, XQ24, XQ27, XQ30, XQ32, X5; :: thesis:

end;

QX4: for i being Nat st 1 <= i & i <= (len (m | n)) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) )

proof

let i be Nat; :: thesis:
assume XQ21: ( 1 <= i & i <= (len (m | n)) - 1 ) ; :: thesis:
then XQ22: (l | n) . i = l . i by PD26;
XQ23: prodi1 . i = prodi . i by PD26, XQ21;
XQ24: prodc1 . i = prodc . i by PD26, XQ21;
XQ25: 1 <= i + 1 by NAT_1:12;
i + 1 <= ((len (m | n)) - 1) + 1 by XQ21, XREAL_1:6;
then YY1: i + 1 in Seg (len (m | n)) by XQ25;
then XQ27: (l | n) . (i + 1) = l . (i + 1) by FUNCT_1:49, PD12;
XQ30: ( 1 <= i & i <= (len m) - 1 ) by X5, AS2, XQ21, PD12, QKK, XXREAL_0:2;
nlist1 . (i + 1) = nlist . (i + 1) by FUNCT_1:49, PD12, YY1;
hence ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | n) . i)) * (prodi1 . i)) mod u1 & (l | n) . (i + 1) = ((l | n) . i) + (u * (prodc1 . i)) ) by XQ22, XQ23, XQ24, XQ27, XQ30, X5; :: thesis:

end;

reconsider s = ((l | n) . (len (m | n))) mod M1 as Element of INT by INT_1:def 2;
QX12: 1 <= (len m) - 1 by X5, AS2, NAT_1:14, NN1;
reconsider lm1 = (len m) - 1 as Element of NAT by X5;
QX13: ( 1 <= lm1 & lm1 <= (len m) - 1 ) by X5, AS2, NAT_1:14, NN1;
consider d, x, y being Element of INT such that
QX14: ( x = (nlist . lm1) `2 & m . (lm1 + 1) = (m . lm1) * x & y = m . (lm1 + 1) & d = (nlist . (lm1 + 1)) `2 & prodi . lm1 = ALGO_INVERSE (y,d) & prodc . lm1 = y ) by X5, AS2, NN2;
consider u, u0, u1 being Element of INT such that
QX15: ( u0 = (nlist . (lm1 + 1)) `1 & u1 = (nlist . (lm1 + 1)) `2 & u = ((u0 - (l . lm1)) * (prodi . lm1)) mod u1 & l . (lm1 + 1) = (l . lm1) + (u * (prodc . lm1)) ) by QX13, X5;
QX43: len nlist in Seg (len nlist) by FINSEQ_1:3;
QX45: M0 = b . (len nlist) by X5, AS2, QX43;
then QX37B: M0 <> 0 by QX43, AS2;
QX36A: (u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0)) is Element of INT by INT_1:def 2;
consider r being Element of INT such that
QX37: u = ((u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0))) + (r * M0) by LmTh4, X5, QX14, QX15, QX36A, QX37B;
QX26A: y <> 0 by QX14, X5, AS2, LmTh5A, LmTh54, LmTh55;

now :: thesis:

per cases ;

suppose AA1: len nlist1 = 1 ; :: thesis:

AAA1: ALGO_CRT nlist1 = (nlist1 . 1) `1 by AA1, defALGOCRT
.= (nlist . 1) `1 by FUNCT_1:49, PD24
.= l . ((len m) - 1) by AA1, AS2, X5, D23, FINSEQ_1:def 3 ;
QX27: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * y)) mod M by QX14, QX15, X5;
reconsider p = 0 as Element of INT by INT_1:def 2;
QX28: ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) by AAA1;
reconsider uy = u * y as Element of INT by INT_1:def 2;
reconsider llm1 = l . ((len m) - 1) as Element of INT by INT_1:def 2;
reconsider ly = llm1 + uy as Element of INT by INT_1:def 2;
M = y * M0 by X5, QX14;
then consider t being Element of INT such that
QX30: ALGO_CRT nlist = ly + (t * M) by LmTh4, QX27, QX37B, QX26A, XCMPLX_1:6;
reconsider qr = r + t as Element of INT by INT_1:def 2;
ALGO_CRT nlist = (((ALGO_CRT nlist1) - (((llm1 * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) by X5, QX14, QX37, QX30, AAA1;
hence ex p, qr being Element of INT st
( ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) & ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) ) by QX28; :: thesis:

end;

suppose AA2: len nlist1 <> 1 ; :: thesis:

then QX7: ALGO_CRT nlist1 = s by defALGOCRT, QX1, QX2, QX4, PD26X
.= ((l | n) . (len (m | n))) mod ((prodc1 . ((len (m | n)) - 1)) * M01) ;
QX8: (l | n) . (len (l | n)) = l . (len (l | n)) by FUNCT_1:49, NN1, PD02, FINSEQ_1:3
.= l . ((len m) - 1) by X5, AS2, FINSEQ_1:59, KK ;
2 <= len nlist1 by AA2, NAT_1:23;
then 2 - 1 <= (len (m | n)) - 1 by XREAL_1:9, PD12, X1;
then QX90: ( 1 <= nn1 & nn1 <= (len (m | n)) - 1 ) by PD11, FINSEQ_1:def 3;
QX10: M01 = (nlist . (len (m | n))) `2 by FUNCT_1:49, D22, PD12, FINSEQ_1:3
.= (nlist . ((len m) - 1)) `2 by X5, AS2, PD11, FINSEQ_1:def 3 ;
consider d1, x1, y1 being Element of INT such that
QX16: ( x1 = (nlist1 . nn1) `2 & (m | n) . (nn1 + 1) = ((m | n) . nn1) * x1 & y1 = (m | n) . (nn1 + 1) & d1 = (nlist1 . (nn1 + 1)) `2 & prodi1 . nn1 = ALGO_INVERSE (y1,d1) & prodc1 . nn1 = y1 ) by QX2, QX90;
QX21: len (m | n) = (len m) - 1 by X5, AS2, PD11, FINSEQ_1:def 3;
then QX20: lm1 in Seg (len (m | n)) by QX12;
QX24: ALGO_CRT nlist1 = (l . ((len m) - 1)) mod (y1 * M01) by QX16, QX7, QX21, QX8, AS2, FINSEQ_1:59, X5, KK;
QX24A: ( ALGO_CRT nlist1 is Element of INT & l . ((len m) - 1) is Element of INT & y1 * M01 is Element of INT ) by INT_1:def 2;
QX26: y = y1 * x by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14;
then QX26C: y1 * M01 <> 0 by X5, AS2, LmTh5A, LmTh54, LmTh55, QX10, QX14;
consider p being Element of INT such that
QX30: ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * (y1 * M01)) by QX24, LmTh4, QX24A, QX26A, QX10, QX14, QX26;
QX27: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((prodc . ((len m) - 1)) * M0) by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14, QX15
.= ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((y1 * x) * M0) by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14 ;
( ALGO_CRT nlist is Element of INT & (l . ((len m) - 1)) + (u * (y1 * x)) is Element of INT & (y1 * x) * M0 is Element of INT ) by INT_1:def 2;
then consider q being Element of INT such that
QX31: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) + (q * ((y1 * x) * M0)) by QX27, LmTh4, QX10, QX14, QX26C, XCMPLX_1:6, QX37B;
reconsider qr = r + q as Element of INT by INT_1:def 2;
((ALGO_CRT nlist1) - (p * (y1 * M01))) + (u * (y1 * x)) = ((ALGO_CRT nlist1) - (p * (y1 * x))) + (u * (y1 * x)) by QX10, QX14
.= (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) by QX26, QX37 ;
then ALGO_CRT nlist = ((((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y)) + (q * (y * M0)) by QX16, X5, AS2, FUNCT_1:49, PD12, QX20, QX14, QX31, QX30
.= (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) ;
hence ex p, qr being Element of INT st
( ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) & ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) ) by QX30, QX26, QX10, QX14; :: thesis:

end;

then consider p, qr being Element of INT such that
QX41: ( ALGO_CRT nlist = (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((qr * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) & ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) ) ;
reconsider y0 = y mod M0 as Element of INT by INT_1:def 2;
y0,M0 are_relative_prime by QX37B, LmTh4A, QX14, X5, QX45, LmTh56;
then y0 gcd M0 = 1 by INT_2:def 3;
then QX48: (ALGO_EXGCD (M0,y0)) `3_3 = 1 by Th2;
QX50: ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y)) mod M0 = ((((l . ((len m) - 1)) * ((ALGO_INVERSE (y,M0)) * y)) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:66
.= (((((l . ((len m) - 1)) mod M0) * (((ALGO_INVERSE (y,M0)) * y) mod M0)) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:67
.= (((((l . ((len m) - 1)) mod M0) * (1 mod M0)) mod M0) + ((p * y) mod M0)) mod M0 by QX48, Th3
.= ((((l . ((len m) - 1)) * 1) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:67
.= (ALGO_CRT nlist1) mod M0 by QX41, NAT_D:66 ;
thus for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) :: thesis:

proof

let i be Nat; :: thesis:
assume VA0: i in Seg (len nlist) ; :: thesis:
then VA1: ( 1 <= i & i <= len nlist ) by FINSEQ_1:1;

per cases ;

suppose VA2: i = len nlist ; :: thesis:

VA22: b . i <> 0 by AS2, VA0;
reconsider I0 = 0 as Element of INT by INT_1:def 2;
reconsider K1y = (((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y) as Element of INT by INT_1:def 2;
reconsider K2y = (qr * y) * M0 as Element of INT by INT_1:def 2;
reconsider K3y = u0 * ((ALGO_INVERSE (y,M0)) * y) as Element of INT by INT_1:def 2;
reconsider K4y = K2y + K3y as Element of INT by INT_1:def 2;
VA31: K2y mod (b . i) = (((qr * y) mod M0) * (M0 mod M0)) mod M0 by QX45, VA2, NAT_D:67
.= (((qr * y) mod M0) * I0) mod M0 by INT_1:50
.= I0 mod (b . i) by VA2, X5, AS2, QX43 ;
VA30: K4y mod (b . i) = ((I0 mod (b . i)) + (K3y mod (b . i))) mod (b . i) by VA31, NAT_D:66
.= (I0 + K3y) mod (b . i) by NAT_D:66
.= ((u0 mod (b . i)) * (((ALGO_INVERSE (y,M0)) * y) mod (b . i))) mod (b . i) by NAT_D:67
.= ((u0 mod (b . i)) * (1 mod (b . i))) mod (b . i) by QX48, Th3, VA2, QX45
.= (u0 * 1) mod (b . i) by NAT_D:67
.= (a . i) mod (b . i) by VA2, QX43, X5, AS2, QX15 ;
VA31: ((ALGO_CRT nlist) + K1y) mod (b . i) = (((ALGO_CRT nlist) mod (b . i)) + ((ALGO_CRT nlist1) mod (b . i))) mod (b . i) by QX50, VA2, QX45, NAT_D:66
.= ((ALGO_CRT nlist) + (ALGO_CRT nlist1)) mod (b . i) by NAT_D:66 ;
VA32: ((ALGO_CRT nlist1) + K4y) mod (b . i) = (((ALGO_CRT nlist1) mod (b . i)) + (K4y mod (b . i))) mod (b . i) by NAT_D:66
.= ((ALGO_CRT nlist1) + (a . i)) mod (b . i) by NAT_D:66, VA30 ;
reconsider LL = ((ALGO_CRT nlist1) + (a . i)) mod (b . i) as Element of INT by INT_1:def 2;
reconsider LL1 = (ALGO_CRT nlist) + (ALGO_CRT nlist1) as Element of INT by INT_1:def 2;
reconsider bi = b . i as Element of INT by INT_1:def 2;
consider r being Element of INT such that
VA33: LL = LL1 + (r * bi) by LmTh4, VA22, VA31, VA32, QX41;
reconsider LL2 = (ALGO_CRT nlist1) + (a . i) as Element of INT by INT_1:def 2;
consider s being Element of INT such that
VA34: LL = LL2 + (s * bi) by LmTh4, VA22;
reconsider LL3 = s - r as Element of INT by INT_1:def 2;
VA36: (LL3 * (b . i)) mod (b . i) = ((LL3 mod (b . i)) * ((b . i) mod (b . i))) mod (b . i) by NAT_D:67
.= ((LL3 mod (b . i)) * I0) mod (b . i) by INT_1:50
.= I0 mod (b . i) ;
thus (ALGO_CRT nlist) mod (b . i) = ((a . i) + ((s - r) * (b . i))) mod (b . i) by VA33, VA34
.= (((a . i) mod (b . i)) + (I0 mod (b . i))) mod (b . i) by VA36, NAT_D:66
.= ((a . i) + I0) mod (b . i) by NAT_D:66
.= (a . i) mod (b . i) ; :: thesis:

end;

suppose i <> len nlist ; :: thesis:

then i < len nlist by VA1, XXREAL_0:1;
then i + 1 <= len nlist by NAT_1:13;
then VA22P: (i + 1) - 1 <= (len nlist) - 1 by XREAL_1:9;
then VA22: ( 1 <= i & i <= len nlist1 ) by KK, FINSEQ_1:59, AS2, FINSEQ_1:1, VA0;
VA24: i in Seg (len nlist1) by FINSEQ_1:1, VA22P, AS2, X1, VA1;
reconsider K1 = ((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) + p as Element of INT by INT_1:def 2;
reconsider K2 = (qr * M0) + (u0 * (ALGO_INVERSE (y,M0))) as Element of INT by INT_1:def 2;
reconsider I0 = 0 as Element of INT by INT_1:def 2;
VA27: y mod (b . i) = 0 by X1, QX14, LmTh6, LmTh54, LmTh55, AS2, X5, VA22;
reconsider K1y = K1 * y as Element of INT by INT_1:def 2;
reconsider K2y = K2 * y as Element of INT by INT_1:def 2;
VA29: (K1 * y) mod (b . i) = ((K1 mod (b . i)) * (y mod (b . i))) mod (b . i) by NAT_D:67
.= 0 mod (b . i) by VA27 ;
VA30: (K2 * y) mod (b . i) = ((K2 mod (b . i)) * (y mod (b . i))) mod (b . i) by NAT_D:67
.= 0 mod (b . i) by VA27 ;
VA31: ((ALGO_CRT nlist) + K1y) mod (b . i) = (((ALGO_CRT nlist) mod (b . i)) + (K1y mod (b . i))) mod (b . i) by NAT_D:66
.= ((ALGO_CRT nlist) + I0) mod (b . i) by NAT_D:66, VA29
.= (ALGO_CRT nlist) mod (b . i) ;
((ALGO_CRT nlist1) + K2y) mod (b . i) = (((ALGO_CRT nlist1) mod (b . i)) + (K2y mod (b . i))) mod (b . i) by NAT_D:66
.= ((ALGO_CRT nlist1) + I0) mod (b . i) by NAT_D:66, VA30
.= (ALGO_CRT nlist1) mod (b . i) ;
hence (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by VA24, QX41, VA31, X400; :: thesis:

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(P0, P1);
hence 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_relative_prime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) ; :: thesis: