per cases
( len nlist = 1 or len nlist <> 1 )
;

end;

suppose A1:
len nlist = 1
; :: thesis: ex b_{1} being Element of INT st

( ( len nlist = 1 implies b_{1} = (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_{1} = (n . (len m)) mod M ) ) )

( ( len nlist = 1 implies b

( 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

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_{1} being Element of INT st

( ( len nlist = 1 implies b_{1} = (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_{1} = (n . (len m)) mod M ) ) )
by A1; :: thesis: verum

end;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

( ( len nlist = 1 implies b

( 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

suppose A2:
len nlist <> 1
; :: thesis: ex b_{1} being Element of INT st

( ( len nlist = 1 implies b_{1} = (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_{1} = (n . (len m)) mod M ) ) )

( ( len nlist = 1 implies b

( 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

defpred S_{1}[ 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_{1}[n,z,y]

A5: ( len m = len nlist & ( m . 1 = i1 or len nlist = 0 ) & ( for i being Nat st 1 <= i & i < len nlist holds

S_{1}[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 )

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_{2}[ 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_{2}[n,z]

A14: ( dom prodi = Seg lm & ( for k being Nat st k in Seg lm holds

S_{2}[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) )_{3}[ 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_{3}[n,z]

A20: ( dom prodc = Seg lm & ( for k being Nat st k in Seg lm holds

S_{3}[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 )

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_{4}[ 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_{4}[n,z,y]

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_{4}[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)) )

( M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & s = (n . (len m)) mod M ) ;

hence ex b_{1} being Element of INT st

( ( len nlist = 1 implies b_{1} = (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_{1} = (n . (len m)) mod M ) ) )
by A2, A28, A22, A5, A27, A15, A21; :: thesis: verum

end;( 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

proof

consider m being FinSequence of INT such that
let n be Nat; :: thesis: ( 1 <= n & n < len nlist implies for z being Element of INT ex y being Element of INT st S_{1}[n,z,y] )

assume A4: ( 1 <= n & n < len nlist ) ; :: thesis: for z being Element of INT ex y being Element of INT st S_{1}[n,z,y]

let z be Element of INT ; :: thesis: ex y being Element of INT st S_{1}[n,z,y]

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: S_{1}[n,z,y]

thus S_{1}[n,z,y]
; :: thesis: verum

end;assume A4: ( 1 <= n & n < len nlist ) ; :: thesis: for z being Element of INT ex y being Element of INT st S

let z be Element of INT ; :: thesis: ex y being Element of INT st S

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: S

thus S

A5: ( len m = len nlist & ( m . 1 = i1 or len nlist = 0 ) & ( for i being Nat st 1 <= i & i < len nlist holds

S

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

A9:
1 <= len m
by A5, NAT_1:14;
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 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: verum

end;( 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 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: verum

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

( 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

proof

consider prodi being FinSequence of INT such that
let n be Nat; :: thesis: ( n in Seg lm implies ex z being Element of INT st S_{2}[n,z] )

assume A11: n in Seg lm ; :: thesis: ex z being Element of INT st S_{2}[n,z]

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: S_{2}[n,w]

thus S_{2}[n,w]
by A13; :: thesis: verum

end;assume A11: n in Seg lm ; :: thesis: ex z being Element of INT st S

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: S

thus S

A14: ( dom prodi = Seg lm & ( for k being Nat st k in Seg lm holds

S

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

defpred S
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;( 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

( 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

proof

consider prodc being FinSequence of INT such that
let n be Nat; :: thesis: ( n in Seg lm implies ex z being Element of INT st S_{3}[n,z] )

assume A18: n in Seg lm ; :: thesis: ex z being Element of INT st S_{3}[n,z]

( 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: S_{3}[n,w]

thus S_{3}[n,w]
by A19; :: thesis: verum

end;assume A18: n in Seg lm ; :: thesis: ex z being Element of INT st S

( 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: S

thus S

A20: ( dom prodc = Seg lm & ( for k being Nat st k in Seg lm holds

S

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

len m in dom nlist
by A5, A9, FINSEQ_3:25;
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;( 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

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

( 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

proof

1 in dom nlist
by A9, A5, FINSEQ_3:25;
let n be Nat; :: thesis: ( 1 <= n & n < len nlist implies for z being Element of INT ex y being Element of INT st S_{4}[n,z,y] )

assume A25: ( 1 <= n & n < len nlist ) ; :: thesis: for z being Element of INT ex y being Element of INT st S_{4}[n,z,y]

let z be Element of INT ; :: thesis: ex y being Element of INT st S_{4}[n,z,y]

( 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: S_{4}[n,z,y]

thus S_{4}[n,z,y]
; :: thesis: verum

end;assume A25: ( 1 <= n & n < len nlist ) ; :: thesis: for z being Element of INT ex y being Element of INT st S

let z be Element of INT ; :: thesis: ex y being Element of INT st S

( 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: S

thus S

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

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

reconsider s = (n . (len m)) mod M as Element of INT by INT_1:def 2;
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 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: verum

end;( 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 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: verum

( M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & s = (n . (len m)) mod M ) ;

hence ex b

( ( len nlist = 1 implies b

( 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