suppose A1: len nlist = 1 ; :: thesis:

then 1 in Seg (len nlist) ;
then 1 in dom nlist by FINSEQ_1:def 3;
then nlist . 1 in [:INT,INT:] by FINSEQ_2:11;
then (nlist . 1) `1 is Element of INT by MCART_1:10;
hence ex b₁ being Element of INT st
( ( len nlist = 1 implies b₁ = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = 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 & n . 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 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b₁ = (n . (len m)) mod M ) ) ) by A1; :: thesis:

end;

suppose A2: len nlist <> 1 ; :: thesis:

defpred S₁[ Nat, Integer, Integer] means ex x being Element of INT st
( x = (nlist . $1) `2 & $3 = $2 * x );
reconsider i1 = 1 as Element of INT by INT_1:def 1;
X1: for n being Element of NAT st 1 <= n & n < len nlist holds
for z being Element of INT ex y being Element of INT st S₁[n,z,y]

proof

let n be Element of NAT ; :: thesis:
assume X11: ( 1 <= n & n < len nlist ) ; :: thesis:
let z be Element of INT ; :: thesis:
n in Seg (len nlist) by X11;
then n in dom nlist by FINSEQ_1:def 3;
then nlist . n in [:INT,INT:] by FINSEQ_2:11;
then reconsider x = (nlist . n) `2 as Element of INT by MCART_1:10;
reconsider y = z * x as Element of INT by INT_1:def 2;
take y ; :: thesis:
thus S₁[n,z,y] ; :: thesis:

end;

consider m being FinSequence of INT such that
X2: ( len m = len nlist & ( m . 1 = i1 or len nlist = 0 ) & ( for i being Element of NAT st 1 <= i & i < len nlist holds
S₁[i,m . i,m . (i + 1)] ) ) from RECDEF_1:sch 4(X1);
II: (len m) - 1 < (len m) - 0 by XREAL_1:15;
X3: for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x )

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i <= (len m) - 1 ) ; :: thesis:
then X32: ( 1 <= i & i < len nlist ) by X2, II, XXREAL_0:2;
i is Element of NAT by ORDINAL1:def 12;
hence ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) by X2, X32; :: thesis:

end;

VV2: 1 <= len m by NAT_1:14, X2;
then 1 - 1 <= (len m) - 1 by XREAL_1:9;
then reconsider lm = (len m) - 1 as Element of NAT by INT_1:3;
defpred S₂[ Nat, Integer] means ex d, x, y being Element of INT st
( x = (nlist . $1) `2 & m . ($1 + 1) = (m . $1) * x & y = m . ($1 + 1) & d = (nlist . ($1 + 1)) `2 & $2 = ALGO_INVERSE (y,d) );
X4: for n being Nat st n in Seg lm holds
ex z being Element of INT st S₂[n,z]

proof

let n be Nat; :: thesis:
assume X41: n in Seg lm ; :: thesis:
X43: ( 1 <= n & n <= (len m) - 1 ) by FINSEQ_1:1, X41;
then consider x being Element of INT such that
X42: ( x = (nlist . n) `2 & m . (n + 1) = (m . n) * x ) by X3;
reconsider y = m . (n + 1) as Element of INT by INT_1:def 2;
n + 1 <= ((len m) - 1) + 1 by X43, XREAL_1:6;
then ( 1 <= n + 1 & n + 1 <= len m ) by NAT_1:12;
then n + 1 in Seg (len nlist) by X2;
then n + 1 in dom nlist by FINSEQ_1:def 3;
then nlist . (n + 1) in [:INT,INT:] by FINSEQ_2:11;
then reconsider d = (nlist . (n + 1)) `2 as Element of INT by MCART_1:10;
reconsider w = ALGO_INVERSE (y,d) as Element of INT ;
take w ; :: thesis:
thus S₂[n,w] by X42; :: thesis:

end;

consider prodi being FinSequence of INT such that
X5: ( dom prodi = Seg lm & ( for k being Nat st k in Seg lm holds
S₂[k,prodi . k] ) ) from FINSEQ_1:sch 5(X4);
X6: len prodi = (len nlist) - 1 by X2, FINSEQ_1:def 3, X5;
X7: 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) )

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i <= (len m) - 1 ) ; :: thesis:
then i in Seg lm by FINSEQ_1:1;
hence 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) ) by X5; :: thesis:

end;

defpred S₃[ Nat, Integer] means ex d, x, y being Element of INT st
( x = (nlist . $1) `2 & m . ($1 + 1) = (m . $1) * x & y = m . ($1 + 1) & d = (nlist . ($1 + 1)) `2 & prodi . $1 = ALGO_INVERSE (y,d) & $2 = y );
X8: for n being Nat st n in Seg lm holds
ex z being Element of INT st S₃[n,z]

proof

let n be Nat; :: thesis:
assume X41: n in Seg lm ; :: thesis:
( 1 <= n & n <= (len m) - 1 ) by FINSEQ_1:1, X41;
then consider d, x, y being Element of INT such that
X42: ( x = (nlist . n) `2 & m . (n + 1) = (m . n) * x & y = m . (n + 1) & d = (nlist . (n + 1)) `2 & prodi . n = ALGO_INVERSE (y,d) ) by X7;
reconsider w = y as Element of INT ;
take w ; :: thesis:
thus S₃[n,w] by X42; :: thesis:

end;

consider prodc being FinSequence of INT such that
X9: ( dom prodc = Seg lm & ( for k being Nat st k in Seg lm holds
S₃[k,prodc . k] ) ) from FINSEQ_1:sch 5(X8);
X10: len prodc = (len nlist) - 1 by X2, FINSEQ_1:def 3, X9;
X11: 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 )

proof

end;

len nlist in Seg (len nlist) by FINSEQ_1:3;
then len m in dom nlist by X2, FINSEQ_1:def 3;
then nlist . (len m) in [:INT,INT:] by FINSEQ_2:11;
then reconsider M0 = (nlist . (len m)) `2 as Element of INT by MCART_1:10;
1 < len m by VV2, A2, X2, XXREAL_0:1;
then 1 + 1 <= len m by NAT_1:13;
then 2 - 1 <= (len m) - 1 by XREAL_1:9;
then VV1: lm in dom prodc by X9;
prodc in INT * by FINSEQ_1:def 11;
then reconsider MM = prodc . ((len m) - 1) as Element of INT by VV1, FINSEQ_1:84;
reconsider M = MM * M0 as Element of INT by INT_1:def 2;
defpred S₄[ Nat, Integer, Integer] means ex u, u0, u1 being Element of INT st
( u0 = (nlist . ($1 + 1)) `1 & u1 = (nlist . ($1 + 1)) `2 & u = ((u0 - $2) * (prodi . $1)) mod u1 & $3 = $2 + (u * (prodc . $1)) );
reconsider i1 = 1 as Element of INT by INT_1:def 1;
X12: for n being Element of NAT st 1 <= n & n < len nlist holds
for z being Element of INT ex y being Element of INT st S₄[n,z,y]

proof

let n be Element of NAT ; :: thesis:
assume X41: ( 1 <= n & n < len nlist ) ; :: thesis:
let z be Element of INT ; :: thesis:
( 1 <= n + 1 & n + 1 <= len m ) by X41, X2, NAT_1:13;
then n + 1 in Seg (len nlist) by X2;
then n + 1 in dom nlist by FINSEQ_1:def 3;
then XX: nlist . (n + 1) in [:INT,INT:] by FINSEQ_2:11;
then reconsider u0 = (nlist . (n + 1)) `1 as Element of INT by MCART_1:10;
reconsider u1 = (nlist . (n + 1)) `2 as Element of INT by XX, MCART_1:10;
reconsider u = ((u0 - z) * (prodi . n)) mod u1 as Element of INT by INT_1:def 2;
reconsider y = z + (u * (prodc . n)) as Element of INT by INT_1:def 2;
take y ; :: thesis:
thus S₄[n,z,y] ; :: thesis:

end;

1 in Seg (len nlist) by VV2, X2;
then 1 in dom nlist by FINSEQ_1:def 3;
then nlist . 1 in [:INT,INT:] by FINSEQ_2:11;
then reconsider L1 = (nlist . 1) `1 as Element of INT by MCART_1:10;
consider n being FinSequence of INT such that
X13: ( len n = len nlist & ( n . 1 = L1 or len nlist = 0 ) & ( for i being Element of NAT st 1 <= i & i < len nlist holds
S₄[i,n . i,n . (i + 1)] ) ) from RECDEF_1:sch 4(X12);
X14: 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 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) )

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i <= (len m) - 1 ) ; :: thesis:
then X32: ( 1 <= i & i < len nlist ) by X2, II, XXREAL_0:2;
i is Element of NAT by ORDINAL1:def 12;
hence ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) by X13, X32; :: thesis:

end;

reconsider s = (n . (len m)) mod M as Element of INT by INT_1:def 2;
( M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & s = (n . (len m)) mod M ) ;
hence ex b₁ being Element of INT st
( ( len nlist = 1 implies b₁ = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = 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 & n . 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 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & b₁ = (n . (len m)) mod M ) ) ) by A2, X14, X11, X2, X13, X6, X10; :: thesis:

end;