per cases ( len nlist = 1 or len nlist <> 1 ) ;
suppose A1: len nlist = 1 ; :: thesis: ex b1 being Element of INT st
( ( len nlist = 1 implies b1 = (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)) ) ) & b1 = (n . (len m)) mod M ) ) )

then 1 in dom nlist by FINSEQ_3:25;
then nlist . 1 in by FINSEQ_2:11;
then (nlist . 1) `1 is Element of INT by MCART_1:10;
hence ex b1 being Element of INT st
( ( len nlist = 1 implies b1 = (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)) ) ) & b1 = (n . (len m)) mod M ) ) ) by A1; :: thesis: verum
end;
suppose A2: len nlist <> 1 ; :: thesis: ex b1 being Element of INT st
( ( len nlist = 1 implies b1 = (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)) ) ) & b1 = (n . (len m)) mod M ) ) )

defpred S1[ 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 S1[n,z,y]
proof
let n be Nat; :: thesis: ( 1 <= n & n < len nlist implies for z being Element of INT ex y being Element of INT st S1[n,z,y] )
assume A4: ( 1 <= n & n < len nlist ) ; :: thesis: for z being Element of INT ex y being Element of INT st S1[n,z,y]
let z be Element of INT ; :: thesis: ex y being Element of INT st S1[n,z,y]
n in dom nlist by ;
then nlist . n in 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: S1[n,z,y]
thus S1[n,z,y] ; :: thesis: verum
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
S1[i,m . i,m . (i + 1)] ) ) from 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: ( 1 <= i & i <= (len m) - 1 implies ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) )

assume ( 1 <= i & i <= (len m) - 1 ) ; :: thesis: ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x )

then ( 1 <= i & i < len nlist ) by ;
hence ex x being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x ) by A5; :: thesis: verum
end;
A9: 1 <= len m by ;
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 S2[ 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 S2[n,z]
proof
let n be Nat; :: thesis: ( n in Seg lm implies ex z being Element of INT st S2[n,z] )
assume A11: n in Seg lm ; :: thesis: ex z being Element of INT st S2[n,z]
A12: ( 1 <= n & n <= (len m) - 1 ) by ;
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 ;
then n + 1 in dom nlist by ;
then nlist . (n + 1) in 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: S2[n,w]
thus S2[n,w] by A13; :: thesis: verum
end;
consider prodi being FinSequence of INT such that
A14: ( dom prodi = Seg lm & ( for k being Nat st k in Seg lm holds
S2[k,prodi . k] ) ) from A15: len prodi = (len nlist) - 1 by ;
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: ( 1 <= i & i <= (len m) - 1 implies 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) ) )

assume ( 1 <= i & i <= (len m) - 1 ) ; :: thesis: 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) )

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: verum
end;
defpred S3[ 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 S3[n,z]
proof
let n be Nat; :: thesis: ( n in Seg lm implies ex z being Element of INT st S3[n,z] )
assume A18: n in Seg lm ; :: thesis: ex z being Element of INT st S3[n,z]
( 1 <= n & n <= (len m) - 1 ) by ;
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: S3[n,w]
thus S3[n,w] by A19; :: thesis: verum
end;
consider prodc being FinSequence of INT such that
A20: ( dom prodc = Seg lm & ( for k being Nat st k in Seg lm holds
S3[k,prodc . k] ) ) from A21: len prodc = (len nlist) - 1 by ;
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
let i be Nat; :: thesis: ( 1 <= i & i <= (len m) - 1 implies 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 ) )

assume ( 1 <= i & i <= (len m) - 1 ) ; :: thesis: 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 )

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) & prodc . i = y ) by A20; :: thesis: verum
end;
len m in dom nlist by ;
then nlist . (len m) in by FINSEQ_2:11;
then reconsider M0 = (nlist . (len m)) `2 as Element of INT by MCART_1:10;
1 < len m by ;
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 ;
reconsider M = MM * M0 as Element of INT by INT_1:def 2;
defpred S4[ 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 S4[n,z,y]
proof
let n be Nat; :: thesis: ( 1 <= n & n < len nlist implies for z being Element of INT ex y being Element of INT st S4[n,z,y] )
assume A25: ( 1 <= n & n < len nlist ) ; :: thesis: for z being Element of INT ex y being Element of INT st S4[n,z,y]
let z be Element of INT ; :: thesis: ex y being Element of INT st S4[n,z,y]
( 1 <= n + 1 & n + 1 <= len m ) by ;
then n + 1 in dom nlist by ;
then A26: nlist . (n + 1) in 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 ;
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: S4[n,z,y]
thus S4[n,z,y] ; :: thesis: verum
end;
1 in dom nlist by ;
then nlist . 1 in 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
S4[i,n . i,n . (i + 1)] ) ) from 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: ( 1 <= i & i <= (len m) - 1 implies 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)) ) )

assume ( 1 <= i & i <= (len m) - 1 ) ; :: thesis: 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)) )

then A29: ( 1 <= i & i < len nlist ) by ;
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 ; :: thesis: verum
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 b1 being Element of INT st
( ( len nlist = 1 implies b1 = (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)) ) ) & b1 = (n . (len m)) mod M ) ) ) by A2, A28, A22, A5, A27, A15, A21; :: thesis: verum
end;
end;