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

then 1 in dom nlist by FINSEQ_3:25;
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;
A3: for n being 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 Nat; :: thesis:
assume A4: ( 1 <= n & n < len nlist ) ; :: thesis:
let z be Element of INT ; :: thesis:
n in dom nlist by A4, FINSEQ_3:25;
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
A5: ( len m = len nlist & ( m . 1 = i1 or len nlist = 0 ) & ( for i being Nat st 1 <= i & i < len nlist holds
S₁[i,m . i,m . (i + 1)] ) ) from RECDEF_1:sch 4(A3);
A6: (len m) - 1 < (len m) - 0 by XREAL_1:15;
A7: 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 ( 1 <= i & i < len nlist ) by A5, A6, XXREAL_0:2;
hence ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) by A5; :: thesis:

end;

A9: 1 <= len m by A5, NAT_1:14;
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) );
A10: 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 A11: n in Seg lm ; :: thesis:
A12: ( 1 <= n & n <= (len m) - 1 ) by A11, FINSEQ_1:1;
then consider x being Element of INT such that
A13: ( x = (nlist . n) `2 & m . (n + 1) = (m . n) * x ) by A7;
reconsider y = m . (n + 1) as Element of INT by INT_1:def 2;
n + 1 <= ((len m) - 1) + 1 by A12, XREAL_1:6;
then n + 1 in dom nlist by A5, FINSEQ_3:25, NAT_1:12;
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 A13; :: thesis:

end;

consider prodi being FinSequence of INT such that
A14: ( dom prodi = Seg lm & ( for k being Nat st k in Seg lm holds
S₂[k,prodi . k] ) ) from FINSEQ_1:sch 5(A10);
A15: len prodi = (len nlist) - 1 by A5, A14, FINSEQ_1:def 3;
A16: 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 ;
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 A14; :: 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 );
A17: 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 A18: n in Seg lm ; :: thesis:
( 1 <= n & n <= (len m) - 1 ) by A18, FINSEQ_1:1;
then consider d, x, y being Element of INT such that
A19: ( 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 A16;
reconsider w = y as Element of INT ;
take w ; :: thesis:
thus S₃[n,w] by A19; :: thesis:

end;

consider prodc being FinSequence of INT such that
A20: ( dom prodc = Seg lm & ( for k being Nat st k in Seg lm holds
S₃[k,prodc . k] ) ) from FINSEQ_1:sch 5(A17);
A21: len prodc = (len nlist) - 1 by A5, A20, FINSEQ_1:def 3;
A22: 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 m in dom nlist by A5, A9, FINSEQ_3:25;
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 A9, A2, A5, XXREAL_0:1;
then 1 + 1 <= len m by NAT_1:13;
then 2 - 1 <= (len m) - 1 by XREAL_1:9;
then A23: lm in dom prodc by A20;
prodc in INT * by FINSEQ_1:def 11;
then reconsider MM = prodc . ((len m) - 1) as Element of INT by A23, 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;
A24: for n being 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 Nat; :: thesis:
assume A25: ( 1 <= n & n < len nlist ) ; :: thesis:
let z be Element of INT ; :: thesis:
( 1 <= n + 1 & n + 1 <= len m ) by A25, A5, NAT_1:13;
then n + 1 in dom nlist by A5, FINSEQ_3:25;
then A26: 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 A26, 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 dom nlist by A9, A5, FINSEQ_3:25;
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
A27: ( len n = len nlist & ( n . 1 = L1 or len nlist = 0 ) & ( for i being Nat st 1 <= i & i < len nlist holds
S₄[i,n . i,n . (i + 1)] ) ) from RECDEF_1:sch 4(A24);
A28: 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 A29: ( 1 <= i & i < len nlist ) by A5, A6, XXREAL_0:2;
thus 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 A27, A29; :: 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, A28, A22, A5, A27, A15, A21; :: thesis:

end;