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_coprime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i);
A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:
let nlist be non empty FinSequence of [:INT,INT:]; :: thesis:
let a, b be FinSequence of INT ; :: thesis:
assume A4: ( 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_coprime ) ) ; :: thesis:

suppose A5: n = 0 ; :: thesis:

A6: 1 in Seg (len nlist) by A5, A4;
A7: ALGO_CRT nlist = (nlist . 1) `1 by Def4, A5, A4
.= a . 1 by A4, A6 ;
thus for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by A7, A5, A4, FINSEQ_1:2, TARSKI:def 1; :: thesis:

end;

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

then A9: 1 <= n by NAT_1:14;
A10: len nlist <> 1 by A4, A8;
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 ;
A11: n <= n + 1 by NAT_1:11;
then A12: len a1 = n by A4, FINSEQ_1:59;
A13: len nlist1 = n by A11, A4, FINSEQ_1:59;
reconsider nlist1 = nlist1 as non empty FinSequence of [:INT,INT:] by A8;
A14: dom nlist1 = Seg (len nlist1) by FINSEQ_1:def 3
.= Seg n by A11, A4, FINSEQ_1:59 ;
n in NAT by ORDINAL1:def 12;
then A15: len nlist1 = n by A14, FINSEQ_1:def 3;
then A16: Seg (len nlist1) c= Seg (len nlist) by A11, A4, FINSEQ_1:5;
A17: ( len nlist1 = n & len a1 = len b1 & len a1 = len nlist1 ) by A12, A11, A4, FINSEQ_1:59;
A18: for i being Nat st i in Seg (len nlist1) holds
b1 . i <> 0

proof

let i be Nat; :: thesis:
assume A19: i in Seg (len nlist1) ; :: thesis:
then b1 . i = b . i by A15, FUNCT_1:49;
hence b1 . i <> 0 by A16, A19, A4; :: thesis:

end;

A20: 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 A21: i in Seg (len nlist1) ; :: thesis:
A22: (nlist1 . i) `1 = (nlist . i) `1 by A21, A15, FUNCT_1:49
.= a . i by A21, A16, A4
.= a1 . i by A21, A15, FUNCT_1:49 ;
(nlist1 . i) `2 = (nlist . i) `2 by A21, A15, FUNCT_1:49
.= b . i by A21, A16, A4
.= b1 . i by A21, A15, FUNCT_1:49 ;
hence ( (nlist1 . i) `1 = a1 . i & (nlist1 . i) `2 = b1 . i ) by A22; :: thesis:

end;

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

proof

let i, j be Nat; :: thesis:
assume A24: ( i in Seg (len nlist1) & j in Seg (len nlist1) & i <> j ) ; :: thesis:
A25: b . i = b1 . i by A24, A15, FUNCT_1:49;
b . j = b1 . j by A24, A15, FUNCT_1:49;
hence b1 . i,b1 . j are_coprime by A25, A24, A16, A4; :: thesis:

end;

A26: 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 A27: i in Seg (len nlist1) ; :: thesis:
then ( a1 . i = a . i & b1 . i = b . i ) by A15, FUNCT_1:49;
hence (ALGO_CRT nlist1) mod (b . i) = (a . i) mod (b . i) by A3, A17, A20, A23, A18, A27; :: thesis:

end;

consider m, l, prodc, prodi being FinSequence of INT , M0, M being Element of INT such that
A28: ( 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 A10, Def4;
A29: 1 + 1 <= n + 1 by A9, XREAL_1:6;
reconsider lb1 = (len b) - 1 as Nat by A4;
A30: ( 1 <= lb1 & lb1 <= lb1 ) by A4, A8, NAT_1:14;
A31: for i being Nat st 1 <= i & i <= lb1 holds
m . (i + 1) = (m . i) * (b . i)

proof

let i be Nat; :: thesis:
assume A32: ( 1 <= i & i <= lb1 ) ; :: thesis:
then A33: 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 A4, A28;
i in Seg (len nlist1) by A32, A13, A4;
hence m . (i + 1) = (m . i) * (b . i) by A33, A4, A16; :: thesis:

end;

A34: m . (len nlist),b . (len nlist) are_coprime by A4, Lm16, A29, A28, A30, A31;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
set l1 = l | nn;
set m1 = m | nn;
A35: n <= n + 1 by NAT_1:11;
then A36: len (l | nn) = n by A4, A28, FINSEQ_1:59;
A37: dom (m | nn) = Seg (len (m | nn)) by FINSEQ_1:def 3
.= Seg n by A4, A28, A35, FINSEQ_1:59 ;
A38: len (m | nn) = n by A37, FINSEQ_1:def 3;
1 - 1 <= n - 1 by A9, XREAL_1:9;
then reconsider nn1 = n - 1 as Element of NAT by INT_1:3;
reconsider prodi1 = prodi | nn1 as FinSequence of INT ;
reconsider prodc1 = prodc | nn1 as FinSequence of INT ;
A39: n - 1 <= n - 0 by XREAL_1:10;
then A40: len prodi1 = nn1 by A4, A28, FINSEQ_1:59;
A41: len prodc1 = nn1 by A39, A4, A28, FINSEQ_1:59;
A42: 1 in Seg n by A9;
A43: (l | nn) . 1 = l . 1 by A42, FUNCT_1:49
.= (nlist1 . 1) `1 by A42, A28, FUNCT_1:49 ;
A44: n - 1 <= n - 0 by XREAL_1:10;

A45: now :: thesis:

let i be Nat; :: thesis:
assume A46: ( 1 <= i & i <= (len (m | nn)) - 1 ) ; :: thesis:
then A47: ( 1 <= i & i <= len (m | nn) ) by A38, A44, XXREAL_0:2;
then i in Seg (len (m | nn)) ;
hence (m | nn) . i = m . i by A38, FUNCT_1:49; :: thesis:
i in Seg (len (l | nn)) by A47, A36, A38;
hence (l | nn) . i = l . i by A36, FUNCT_1:49; :: thesis:
i in Seg (len prodi1) by A46, A38, A40;
hence prodi1 . i = prodi . i by A40, FUNCT_1:49; :: thesis:
i in Seg (len prodc1) by A46, A38, A41;
hence prodc1 . i = prodc . i by A41, FUNCT_1:49; :: thesis:

end;

len (m | nn) in Seg (len nlist1) by A13, A38, FINSEQ_1:3;
then A48: len (m | nn) in Seg (len nlist) by A16;
A49: nlist1 . (len (m | nn)) = nlist . (len (m | nn)) by A13, A38, FINSEQ_1:3, FUNCT_1:49;
len (m | nn) in dom nlist by A48, FINSEQ_1:def 3;
then nlist1 . (len (m | nn)) in [:INT,INT:] by A49, FINSEQ_2:11;
then reconsider M01 = (nlist1 . (len (m | nn))) `2 as Element of INT by MCART_1:10;
reconsider M1 = (prodc1 . ((len (m | nn)) - 1)) * M01 as Element of INT by INT_1:def 2;
A50: ( len (m | nn) = len nlist1 & len (l | nn) = len nlist1 & len prodc1 = (len nlist1) - 1 & len prodi1 = (len nlist1) - 1 & (m | nn) . 1 = 1 ) by A35, A4, A38, A36, A41, A40, A28, A42, FINSEQ_1:59, FUNCT_1:49;
A51: for i being Nat st 1 <= i & i <= (len (m | nn)) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | nn) . (i + 1) = ((m | nn) . i) * x & y = (m | nn) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y )

proof

let i be Nat; :: thesis:
assume A52: ( 1 <= i & i <= (len (m | nn)) - 1 ) ; :: thesis:
then A53: (m | nn) . i = m . i by A45;
A54: prodi1 . i = prodi . i by A45, A52;
A55: prodc1 . i = prodc . i by A45, A52;
A56: 1 <= i + 1 by NAT_1:12;
i + 1 <= ((len (m | nn)) - 1) + 1 by A52, XREAL_1:6;
then A57: i + 1 in Seg (len (m | nn)) by A56;
then A58: (m | nn) . (i + 1) = m . (i + 1) by A38, FUNCT_1:49;
A59: ( 1 <= i & i <= len (m | nn) ) by A52, A38, A44, XXREAL_0:2;
A60: ( 1 <= i & i <= (len m) - 1 ) by A28, A4, A52, A38, A44, XXREAL_0:2;
i in Seg (len nlist1) by A38, A13, A59;
then A61: nlist1 . i = nlist . i by A15, FUNCT_1:49;
nlist1 . (i + 1) = nlist . (i + 1) by A38, A57, FUNCT_1:49;
hence ex d, x, y being Element of INT st
( x = (nlist1 . i) `2 & (m | nn) . (i + 1) = ((m | nn) . i) * x & y = (m | nn) . (i + 1) & d = (nlist1 . (i + 1)) `2 & prodi1 . i = ALGO_INVERSE (y,d) & prodc1 . i = y ) by A53, A54, A55, A58, A60, A61, A28; :: thesis:

end;

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

proof

let i be Nat; :: thesis:
assume A63: ( 1 <= i & i <= (len (m | nn)) - 1 ) ; :: thesis:
then A64: (l | nn) . i = l . i by A45;
A65: prodi1 . i = prodi . i by A45, A63;
A66: prodc1 . i = prodc . i by A45, A63;
A67: 1 <= i + 1 by NAT_1:12;
i + 1 <= ((len (m | nn)) - 1) + 1 by A63, XREAL_1:6;
then A68: i + 1 in Seg (len (m | nn)) by A67;
then A69: (l | nn) . (i + 1) = l . (i + 1) by A38, FUNCT_1:49;
A70: ( 1 <= i & i <= (len m) - 1 ) by A28, A4, A63, A38, A44, XXREAL_0:2;
nlist1 . (i + 1) = nlist . (i + 1) by A38, A68, FUNCT_1:49;
hence ex u, u0, u1 being Element of INT st
( u0 = (nlist1 . (i + 1)) `1 & u1 = (nlist1 . (i + 1)) `2 & u = ((u0 - ((l | nn) . i)) * (prodi1 . i)) mod u1 & (l | nn) . (i + 1) = ((l | nn) . i) + (u * (prodc1 . i)) ) by A64, A65, A66, A69, A70, A28; :: thesis:

end;

reconsider s = ((l | nn) . (len (m | nn))) mod M1 as Element of INT by INT_1:def 2;
A71: 1 <= (len m) - 1 by A28, A4, A8, NAT_1:14;
reconsider lm1 = (len m) - 1 as Element of NAT by A28;
A72: ( 1 <= lm1 & lm1 <= (len m) - 1 ) by A28, A4, A8, NAT_1:14;
consider d, x, y being Element of INT such that
A73: ( 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 A28, A4, A9;
consider u, u0, u1 being Element of INT such that
A74: ( 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 A72, A28;
A75: len nlist in Seg (len nlist) by FINSEQ_1:3;
A76: M0 = b . (len nlist) by A28, A4, A75;
then A77: M0 <> 0 by A75, A4;
then consider r being Element of INT such that
A79: u = ((u0 - (l . ((len m) - 1))) * (ALGO_INVERSE (y,M0))) + (r * M0) by Lm14, A28, A73, A74;
A80: y <> 0 by A73, A28, A4, Lm15, A30, A31;

now :: thesis:

per cases ;

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

A82: ALGO_CRT nlist1 = (nlist1 . 1) `1 by A81, Def4
.= (nlist . 1) `1 by A42, FUNCT_1:49
.= l . ((len m) - 1) by A81, A4, A28, A14, FINSEQ_1:def 3 ;
A83: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * y)) mod M by A73, A74, A28;
reconsider p = 0 as Element of INT by INT_1:def 2;
A84: ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * y) by A82;
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;
consider t being Element of INT such that
A85: ALGO_CRT nlist = ly + (t * M) by Lm14, A83, A77, A80, XCMPLX_1:6, A28, A73;
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 A28, A73, A79, A85, A82;
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 A84; :: thesis:

end;

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

then A87: ALGO_CRT nlist1 = s by Def4, A50, A51, A62, A43
.= ((l | nn) . (len (m | nn))) mod ((prodc1 . ((len (m | nn)) - 1)) * M01) ;
A88: (l | nn) . (len (l | nn)) = l . (len (l | nn)) by A8, A36, FINSEQ_1:3, FUNCT_1:49
.= l . ((len m) - 1) by A28, A4, A35, FINSEQ_1:59 ;
2 <= len nlist1 by A86, NAT_1:23;
then 2 - 1 <= (len (m | nn)) - 1 by A38, A17, XREAL_1:9;
then A89: ( 1 <= nn1 & nn1 <= (len (m | nn)) - 1 ) by A37, FINSEQ_1:def 3;
A90: M01 = (nlist . (len (m | nn))) `2 by A13, A38, FINSEQ_1:3, FUNCT_1:49
.= (nlist . ((len m) - 1)) `2 by A28, A4, A37, FINSEQ_1:def 3 ;
consider d1, x1, y1 being Element of INT such that
A91: ( x1 = (nlist1 . nn1) `2 & (m | nn) . (nn1 + 1) = ((m | nn) . nn1) * x1 & y1 = (m | nn) . (nn1 + 1) & d1 = (nlist1 . (nn1 + 1)) `2 & prodi1 . nn1 = ALGO_INVERSE (y1,d1) & prodc1 . nn1 = y1 ) by A51, A89;
A92: len (m | nn) = (len m) - 1 by A28, A4, A37, FINSEQ_1:def 3;
then A93: lm1 in Seg (len (m | nn)) by A71;
A94: ALGO_CRT nlist1 = (l . ((len m) - 1)) mod (y1 * M01) by A91, A87, A92, A88, A4, A28, A35, FINSEQ_1:59;
A96: y = y1 * x by A91, A28, A4, A38, A93, A73, FUNCT_1:49;
then A97: y1 * M01 <> 0 by A28, A4, Lm15, A30, A31, A90, A73;
consider p being Element of INT such that
A98: ALGO_CRT nlist1 = (l . ((len m) - 1)) + (p * (y1 * M01)) by A94, Lm14, A80, A90, A73, A96;
ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((prodc . ((len m) - 1)) * M0) by A91, A28, A4, A38, A93, A73, A74, FUNCT_1:49
.= ((l . ((len m) - 1)) + (u * (y1 * x))) mod ((y1 * x) * M0) by A91, A28, A4, A38, A93, A73, FUNCT_1:49 ;
then consider q being Element of INT such that
A100: ALGO_CRT nlist = ((l . ((len m) - 1)) + (u * (y1 * x))) + (q * ((y1 * x) * M0)) by Lm14, A90, A73, A97, A77, XCMPLX_1:6;
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 A90, A73
.= (((ALGO_CRT nlist1) - ((((l . ((len m) - 1)) * (ALGO_INVERSE (y,M0))) * y) + (p * y))) + ((r * M0) * y)) + ((u0 * (ALGO_INVERSE (y,M0))) * y) by A96, A79 ;
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 A91, A28, A4, A38, A93, A73, A100, A98, FUNCT_1:49
.= (((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 A98, A96, A90, A73; :: thesis:

end;

then consider p, qr being Element of INT such that
A101: ( 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 gcd M0 = 1 by INT_2:def 3, A77, Th10, A73, A28, A76, A34;
then A102: (ALGO_EXGCD (M0,y0)) `3_3 = 1 by Th6;
A103: ((((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 A102, Th7
.= ((((l . ((len m) - 1)) * 1) mod M0) + ((p * y) mod M0)) mod M0 by NAT_D:67
.= (ALGO_CRT nlist1) mod M0 by A101, 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 A104: i in Seg (len nlist) ; :: thesis:
then A105: ( 1 <= i & i <= len nlist ) by FINSEQ_1:1;

per cases ;

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

A107: b . i <> 0 by A4, A104;
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;
A108: K2y mod (b . i) = (((qr * y) mod M0) * (M0 mod M0)) mod M0 by A76, A106, NAT_D:67
.= (((qr * y) mod M0) * I0) mod M0 by INT_1:50
.= I0 mod (b . i) by A106, A28, A4, A75 ;
A109: K4y mod (b . i) = ((I0 mod (b . i)) + (K3y mod (b . i))) mod (b . i) by A108, 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 A102, Th7, A106, A76
.= (u0 * 1) mod (b . i) by NAT_D:67
.= (a . i) mod (b . i) by A106, A75, A28, A4, A74 ;
A110: ((ALGO_CRT nlist) + K1y) mod (b . i) = (((ALGO_CRT nlist) mod (b . i)) + ((ALGO_CRT nlist1) mod (b . i))) mod (b . i) by A103, A106, A76, NAT_D:66
.= ((ALGO_CRT nlist) + (ALGO_CRT nlist1)) mod (b . i) by NAT_D:66 ;
A111: ((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 A109, NAT_D:66 ;
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
A112: LL = LL1 + (r * bi) by Lm14, A107, A110, A111, A101;
reconsider LL2 = (ALGO_CRT nlist1) + (a . i) as Element of INT by INT_1:def 2;
consider s being Element of INT such that
A113: LL = LL2 + (s * bi) by Lm14, A107;
reconsider LL3 = s - r as Element of INT by INT_1:def 2;
A114: (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 A112, A113
.= (((a . i) mod (b . i)) + (I0 mod (b . i))) mod (b . i) by A114, 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 A105, XXREAL_0:1;
then i + 1 <= len nlist by NAT_1:13;
then A115: (i + 1) - 1 <= (len nlist) - 1 by XREAL_1:9;
then A116: ( 1 <= i & i <= len nlist1 ) by A35, A4, A104, FINSEQ_1:1, FINSEQ_1:59;
A117: i in Seg (len nlist1) by A115, A4, A17, A105;
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;
A118: y mod (b . i) = 0 by A17, A73, Lm17, A30, A31, A4, A28, A116;
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;
A119: (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 A118 ;
A120: (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 A118 ;
A121: ((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 A119, NAT_D:66
.= (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 A120, NAT_D:66
.= (ALGO_CRT nlist1) mod (b . i) ;
hence (ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) by A117, A101, A121, A26; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
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_coprime ) holds
for i being Nat st i in Seg (len nlist) holds
(ALGO_CRT nlist) mod (b . i) = (a . i) mod (b . i) ; :: thesis: