:: Extended Euclidean Algorithm and CRT Algorithm
::  by Hiroyuki Okazaki , Yosiki Aoki and Yasunari Shidama
:: 
:: Received February 8, 2012
:: Copyright (c) 2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RECDEF_2, TARSKI, XBOOLE_0, FINSEQ_1, RELAT_1, FUNCT_1, COMPLEX1,
      NAT_1, MCART_1, ZFMISC_1, SUBSET_1, NUMBERS, INT_1, INT_2, CARD_1,
      ARYTM_1, XXREAL_0, ARYTM_3, ORDINAL4, NTALGO_1, CARD_3;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, XTUPLE_0, MCART_1,
      FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2, NAT_D,
      FINSEQ_1, RVSUM_1, ORDINAL1;
 constructors XXREAL_0, NAT_D, REAL_1, BINARITH, RVSUM_1, XTUPLE_0;
 registrations XREAL_0, RELSET_1, ORDINAL1, INT_1, SUBSET_1, FINSEQ_1, NAT_1,
      XXREAL_0, XBOOLE_0, VALUED_0, CARD_1, NUMBERS, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
 definitions FINSEQ_1, INT_1, XTUPLE_0;
 theorems TARSKI, ZFMISC_1, FUNCT_1, MCART_1, FUNCT_2, XXREAL_0, XREAL_1,
      NAT_1, INT_1, INT_2, NAT_D, FINSEQ_1, FINSEQ_2, XBOOLE_1, ORDINAL1,
      ABSVALUE, XCMPLX_1, INT_4, RVSUM_1, INT_6, XTUPLE_0, WSIERP_1;
 schemes FINSEQ_1, NAT_1, RECDEF_1, RECDEF_2;

begin :: Euclidean Algorithm

theorem LMTh3: for x,p be Integer holds (x mod p) mod p = x mod p
proof
  let x,p be Integer;
  x mod p = (x + 0) mod p .= ((x mod p) + (0 mod p)) mod p by NAT_D:66
  .= ((x mod p) + 0) mod p by INT_4:12;
  hence thesis;
end;

LM6: for a be Element of NAT
holds a gcd 0 = a
proof
  let a be Element of NAT;
  0 = 0 * a;
  then
  P2: a divides 0 by INT_1:def 3;
  for m being Integer
  st m divides a & m divides 0 holds m divides a;
  hence a gcd 0 = a by P2,INT_2:def 2;
end;

::==========================================================================================
::NZMATH source code
::
::def gcd(a, b):
::    """
::    Return the greatest common divisor of 2 integers a and b.
::    """
::    a, b = abs(a), abs(b)
::    while b:
::        a, b = b, a % b
::    return a
::==========================================================================================

  LM1:for a,b be Element of INT
  holds
  ex A,B be sequence of NAT
  st
  A.0 = abs(a) & B.0 = abs(b)
  &
  (for i be Element of NAT
  holds A.(i+1) = B.i &
  B.(i+1) = A.i mod B.i)
  proof
    let a,b be Element of INT;

    defpred P1[Nat,Nat,Nat,Nat,Nat ]
    means
    $4 = $3 & $5 = $2 mod $3;

    Q1: for n being Element of NAT,
    x being Element of NAT,
    y being Element of NAT
    ex
    x1 being Element of NAT,
    y1 being Element of NAT st P1[n,x,y,x1,y1];

    consider A be Function of NAT,NAT,B be Function of NAT,NAT
    such that P2:
    A.0 = abs(a) & B.0 = abs(b)
    &
    for n being Element of NAT
    holds P1[ n,A.n,B.n,A.(n + 1),B.(n + 1) ]
    from RECDEF_2:sch 3(Q1);
    take A,B;
    thus thesis by P2;
  end;

  LM2:for a,b be Element of INT,
  A1,B1,A2,B2 be sequence of NAT
  st
  ( A1.0 = abs(a) & B1.0 = abs(b)
  &
  (for i be Element of NAT
  holds A1.(i+1) = B1.i &
  B1.(i+1) = A1.i mod B1.i))&
  (A2.0 = abs(a) & B2.0 = abs(b) &
  (for i be Element of NAT holds
  A2.(i+1) = B2.i &
  B2.(i+1) = A2.i mod B2.i)
  )
  holds
  A1 = A2 & B1 = B2
  proof
    let a,b be Element of INT;
    let A1,B1,A2,B2 be sequence of NAT;
    assume P1:
    A1.0 = abs(a) & B1.0 = abs(b)
    &
    for i be Element of NAT
    holds
    A1.(i+1) = B1.i &
    B1.(i+1) = A1.i mod B1.i;

    assume P2:
    A2.0 = abs(a) & B2.0 = abs(b)
    &
    for i be Element of NAT
    holds A2.(i+1) = B2.i &
    B2.(i+1) = A2.i mod B2.i;

    defpred P[Nat] means A1.$1 = A2.$1 & B1.$1 = B2.$1;
    P0: P[0] by P1,P2;
    PN: for n being Element of NAT st P[n] holds P[n+1]
    proof
      let n being Element of NAT;
      assume PN1:P[n];
      PN2: A1.(n+1) = B1.n by P1
      .=A2.(n+1) by P2,PN1;
      B1.(n+1) = A1.n mod B1.n by P1
      .=B2.(n+1) by P2,PN1;
      hence P[n+1] by PN2;
    end;

    for n being Element of NAT holds P[n] from NAT_1:sch 1(P0,PN);
    hence thesis by FUNCT_2:def 8;
  end;

definition
  let a,b be Element of INT;
  func ALGO_GCD(a,b) -> Element of NAT means
  :defALGOGCD:
  ex A,B be sequence of NAT st
  A.0 = abs(a) & B.0 = abs(b) &
  (for i be Element of NAT holds
  A.(i+1) = B.i &
  B.(i+1) = A.i mod B.i) &
  it = A. (min*{i where i is Element of NAT: B.i = 0} );
  existence
  proof
    consider A,B be sequence of NAT
    such that P1:
    A.0 = abs(a) & B.0 = abs(b) &
    (for i be Element of NAT holds
    A.(i+1) = B.i &
    B.(i+1) = A.i mod B.i) by LM1;

    set m = A.(min*{i where i is Element of NAT: B.i = 0});
    m is Element of NAT;
    hence thesis by P1;
  end;

  uniqueness
  proof
    let m1,m2 be Element of NAT;
    assume ex A1,B1 be sequence of NAT
    st A1.0 = abs(a) & B1.0 = abs(b)
    &
    (for i be Element of NAT holds
    A1.(i+1) = B1.i &
    B1.(i+1) = A1.i mod B1.i)&
    m1 = A1.(min*{i where i is Element of NAT: B1.i = 0});
    then
    consider A1,B1 be sequence of NAT
    such that P1:
    A1.0 = abs(a) & B1.0 = abs(b)
    &
    (for i be Element of NAT
    holds A1.(i+1) = B1.i &
    B1.(i+1) = A1.i mod B1.i) &
    m1 = A1.(min*{i where i is Element of NAT: B1.i = 0});
    assume
    ex A2,B2 be sequence of NAT
    st
    A2.0 = abs(a) & B2.0 = abs(b) &
    (for i be Element of NAT holds
    A2.(i+1) = B2.i &
    B2.(i+1) = A2.i mod B2.i) &
    m2 = A2.(min*{i where i is Element of NAT: B2.i = 0});
    then
    consider A2,B2 be sequence of NAT
    such that P2:
    A2.0 = abs(a) & B2.0 = abs(b)
    &
    (for i be Element of NAT holds
    A2.(i+1) = B2.i &
    B2.(i+1) = A2.i mod B2.i) &
    m2 = A2.(min*{i where i is Element of NAT: B2.i = 0});
    A1 = A2 & B1 = B2 by LM2,P1,P2;
    hence thesis by P1,P2;
  end;
end;

LM3:for a,b be Element of INT,
A,B be sequence of NAT st
(A.0 = abs(a) & B.0 = abs(b) &
(for i be Element of NAT holds
A.(i+1) = B.i &
B.(i+1) = A.i mod B.i))
holds
for i be Element of NAT st B.i <> 0
holds A.i gcd B.i = A.(i+1) gcd B.(i+1)
proof
  let a,b be Element of INT,
  A,B be sequence of NAT;
  assume AS:
  A.0 = abs(a) & B.0 = abs(b) &
  (for i be Element of NAT holds
  A.(i+1) = B.i & B.(i+1) = A.i mod B.i);

  let i be Element of NAT;
  assume AS1: B.i <> 0;
  set k=A.i gcd B.i;

  Q1: A.(i+1) = B.i by AS;
  Q2: B.(i+1) = A.i mod B.i by AS;

  P1: k divides A.(i+1) by Q1,INT_2:def 2;

  P2: k divides B.(i+1)
  proof
    X1: B.(i+1) = A.i - (A.i div B.i ) * B.i by INT_1:def 10,Q2,AS1;
    X2: k divides A.i by INT_2:def 2;
    X3: k divides B.i by INT_2:def 2;

    X4:ex s being Integer
    st A.i = k*s by X2,INT_1:def 3;
    ex t being Integer
    st B.i = k*t by X3,INT_1:def 3;
    then
    consider s,t be Integer such that
    X5:B.(i+1) = (k*s) - (A.i div B.i ) * (k*t) by X1,X4;
    B.(i+1) = (s - (A.i div B.i)*t ) * k by X5;
    hence
    k divides B.(i+1) by INT_1:def 3;
  end;

  for m being Integer
  st m divides A.(i+1) & m divides B.(i+1) holds m divides k
  proof
    let m being Integer;
    assume P3: m divides A.(i+1) & m divides B.(i+1);
    then
    P31: m divides B.i by AS;
    P32: m divides A.i
    proof
      B.(i+1) = A.i - (A.i div B.i ) * B.i by INT_1:def 10,Q2,AS1;
      then
      X1: A.i = B.(i+1) + (A.i div B.i ) * B.i;
      X21:ex s being Integer
      st B.i = m * s by INT_1:def 3,P31;
      X22:ex t being Integer
      st B.(i+1) = m * t by INT_1:def 3,P3;
      consider s,t be Integer such that
      X4:A.i = (m*s) + (A.i div B.i ) * (m*t) by X1,X21,X22;
      A.i = m * (s + (A.i div B.i ) * t) by X4;
      hence m divides A.i by INT_1:def 3;
    end;
    thus m divides k by P31,P32,INT_2:def 2;
  end;
  hence
  A.(i+1) gcd B.(i+1) = k by P1,P2,INT_2:def 2;
end;

LM4:for a,b be Element of INT,
A,B be sequence of NAT
st
(A.0 = abs(a) & B.0 = abs(b)
&
(for i be Element of NAT holds
A.(i+1) = B.i &
B.(i+1) = A.i mod B.i))
holds
for i be Element of NAT st B.i <> 0
holds
A.0 gcd B.0 = A.i gcd B.i
proof
  let a,b be Element of INT,
  A,B be sequence of NAT;
  assume AS1:
  A.0 = abs(a) & B.0 = abs(b)
  &
  (for i be Element of NAT holds
  A.(i+1) = B.i &
  B.(i+1) = A.i mod B.i);
  defpred P[Nat] means
  B.$1 <> 0 implies
  A.0 gcd B.0 = A.$1 gcd B.$1;
  P0: P[0];
  PN: for i being Element of NAT st P[i] holds P[i+1]
  proof
    let i being Element of NAT;
    assume PN1: P[i];
    B.(i+1) <> 0 implies
    A.0 gcd B.0 = A.(i+1) gcd B.(i+1)
    proof
      assume PN2: B.(i+1) <> 0;
      B.i <> 0
      proof
        assume PN4: B.i = 0;
        B.(i+1) = A.i mod B.i by AS1;
        hence contradiction by PN2,PN4,INT_1:def 10;
      end;
      hence thesis by PN1,AS1,LM3;
    end;
    hence P[i+1];
  end;
  for i being Element of NAT holds P[i] from NAT_1:sch 1(P0,PN);
  hence thesis;
end;

LM5:for a,b be Element of INT,
A,B be sequence of NAT
st
(A.0 = abs(a) & B.0 = abs(b)
&
(for i be Element of NAT
holds A.(i+1) = B.i &
B.(i+1) = A.i mod B.i))
holds
{i where i is Element of NAT: B.i = 0}
is non empty Subset of NAT
proof
  let a,b be Element of INT,
  A,B be sequence of NAT;
  assume AS1:
  A.0 = abs(a) & B.0 = abs(b)
  &
  (for i be Element of NAT holds
  A.(i+1) = B.i &
  B.(i+1) = A.i mod B.i);
  P1:for x be set st x in
  {i where i is Element of NAT: B.i = 0}
  holds x in NAT
  proof let x be set;
    assume x in {i where i is Element of NAT: B.i = 0};
    then
    ex i be Element of NAT st x=i & B.i = 0;
    hence x in NAT;
  end;

  ex m0 be Element of NAT st B.m0 = 0
  proof
    assume A2:
    not (ex m0 be Element of NAT st B.m0 = 0);

    A3: for i be Element of NAT holds
    B.(i+1) <= B.i -1
    proof
      let i be Element of NAT;
      A31:B.i <> 0 by A2;

      B.(i+1) = A.i mod B.i by AS1;
      then
      B.(i+1) < B.i by A31,INT_1:58;
      then
      B.(i+1) +1 <= B.i by NAT_1:13;
      then
      B.(i+1) +1 -1 <= B.i -1 by XREAL_1:9;
      hence
      B.(i+1) <= B.i -1;
    end;
    defpred P[Nat] means B.$1 <= B.0 - $1;

    P0: P[0];
    P1: for i be Element of NAT st P[i] holds P[i+1]
    proof
      let i be Element of NAT;
      assume P11:P[i];
      P12: B.(i+1) <= B.i -1 by A3;
      B.i -1 <= (B.0 - i) -1 by P11,XREAL_1:9;
      hence P[i+1] by XXREAL_0:2,P12;
    end;

    A4: for i be Element of NAT holds P[i] from NAT_1:sch 1(P0,P1);
    B.(B.0) <=B.0 - (B.0) by A4;
    hence contradiction by A2,NAT_1:14;
  end;
  then
  consider m0 be Element of NAT such that
  X1: B.m0 = 0;
  m0 in {i where i is Element of NAT: B.i = 0} by X1;
  hence thesis by P1,TARSKI:def 3;
end;

theorem ::Th1:
  for a,b be Element of INT
  holds
  ALGO_GCD(a,b) = a gcd b
  proof
    let a,b be Element of INT;
    consider A,B be sequence of NAT such that
    P1:
    A.0 = abs(a) & B.0 = abs(b)
    &
    (for i be Element of NAT holds
    A.(i+1) = B.i &
    B.(i+1) = A.i mod B.i)
    &
    ALGO_GCD(a,b)
    = A. (min*{i where i is Element of NAT: B.i = 0})
    by defALGOGCD;

    set m0= (min*{i where i is Element of NAT: B.i = 0});
    X0: {i where i is Element of NAT: B.i = 0}
    is non empty Subset of NAT by P1,LM5;
    then
    m0 in {i where i is Element of NAT: B.i = 0} by NAT_1:def 1;
    then P4:
    ex i be Element of NAT st m0=i & B.i = 0;

    per cases;
    suppose C1:m0 = 0;
      thus
      ALGO_GCD(a,b) = A.0 gcd B.0 by P4,C1,LM6,P1
      .= a gcd b by INT_2:34,P1;
    end;
    suppose m0 <> 0;
      then
      1 <= m0 by NAT_1:14;
      then
      1-1 <= m0-1 by XREAL_1:9;
      then
      reconsider m1 = m0-1 as Element of NAT by INT_1:3;
      X1: B.m1 <> 0
      proof
        assume B.m1 = 0;
        then
        X11: m1 in {i where i is Element of NAT: B.i = 0};

        m0 -1 < m0 - 0 by XREAL_1:15;
        hence contradiction by X11,X0,NAT_1:def 1;
      end;
      then
      X2: A.0 gcd B.0 = A.m1 gcd B.m1 by P1,LM4;
      P3:A.m1 gcd B.m1 = A.(m1+1) gcd B.(m1+1) by LM3,X1,P1;

      A.m0 gcd B.m0
      =ALGO_GCD(a,b) by P1,LM6,P4;
      hence thesis by P3,INT_2:34,X2,P1;
    end;
  end;

begin ::Extended Euclidean Algorithm
::==========================================================================================
::NZMATH source code
::
:: def extgcd(x,y):
:: """
:: Return a tuple (u,v,d); they are the greatest common divisor d
:: of two integers x and y and u,v such that d = x * u + y * v.
:: """
:: # Crandall & Pomerance "PRIME NUMBERS",Algorithm 2.1.4
:: a,b,g,u,v,w = 1,0,x,0,1,y
:: while w:
:: q,t = divmod(g,w)
:: a,b,g,u,v,w = u,v,w,a-q*u,b-q*v,t
:: if g >= 0:
:: return (a,b,g)
:: else:
:: return (-a,-b,-g)
::==========================================================================================

scheme
  QuadChoiceRec { A,B,C,D() -> non empty set,
  A0() -> Element of A(),B0() -> Element of B(),
  C0() -> Element of C(),D0() -> Element of D(),
  P[set,set,set,set,set,set,set,set,set] }:
  ex f being Function of NAT,A(),g being Function of NAT,B(),
  h being Function of NAT,C(),i being Function of NAT,D()
  st f.0 = A0() & g.0 = B0() &h.0 = C0() & i.0 = D0()
  & for n being Element of
  NAT holds P[n,f.n,g.n,h.n,i.n,f.(n+1),g.(n+1),h.(n+1),i.(n+1)]
  provided
  A1: for n being Element of NAT,x being Element of A(),y being Element
  of B(),z being Element of C(),w being Element of D()
  ex x1 being Element of A(),y1 being Element of B(),
  z1 being Element of C(),w1 being Element of D()
  st P[n,x,y,z,w,x1,y1,z1,w1]
  proof
    defpred P1[set,set,set,set,set]
    means P[$1,($2)`1,($2)`2,($3)`1,($3)`2,($4)`1,($4)`2,($5)`1,($5)`2];
    A2: for n being Element of NAT,x being Element of [:A(),B():],
    y being Element of [:C(),D():]
    ex z being Element of [:A(),B():],w being Element of [:C(),D():]
    st P1[n,x,y,z,w]
    proof
      let n be Element of NAT,x be Element of [:A(),B():],
      y be Element of [:C(),D():];
      x`1 is Element of A() & x`2 is Element of B()
      & y`1 is Element of C() & y`2 is Element of D()
      by MCART_1:10;
      then
      consider ai being Element of A(),bi being Element of B(),
      ci being Element of C(),di being Element of D() such that
      A3: P[n,x`1,x`2,y`1,y`2,ai,bi,ci,di] by A1;
      reconsider z= [ai,bi]
      as Element of [:A(),B():] by ZFMISC_1:87;
      reconsider w= [ci,di]
      as Element of [:C(),D():] by ZFMISC_1:87;
      take z,w;
      [ai,bi]`1 = ai &
      [ai,bi]`2 = bi &
      [ci,di]`1 = ci &
      [ci,di]`2 = di by MCART_1:7;
      hence thesis by A3;
    end;
    reconsider
    AB0=[A0(),B0()] as Element of [:A(),B():] by ZFMISC_1:87;
    reconsider
    CD0=[C0(),D0()] as Element of [:C(),D():] by ZFMISC_1:87;
    consider fg being Function of NAT,[:A(),B():],
    hi being Function of NAT,[:C(),D():] such that
    A4: fg.0 = AB0 and
    A41: hi.0 = CD0 and
    A5: for e being Element of NAT holds P1[e,fg.e,hi.e,fg.(e+1),hi.(e+1)]
    from RECDEF_2:sch 3( A2);
    take pr1 fg,pr2 fg,pr1 hi,pr2 hi;
    (fg.0)`1 = (pr1 fg).0 & (fg.0)`2 = (pr2 fg).0
    & (hi.0)`1 = (pr1 hi).0 & (hi.0)`2 = (pr2 hi).0
    by FUNCT_2:def 5,def 6;
    hence (pr1 fg).0 = A0() & (pr2 fg).0 = B0()
    &(pr1 hi).0 = C0() & (pr2 hi).0 = D0()
    by A4,A41,XTUPLE_0:def 2,def 3;
    let i be Element of NAT;
    A6: (fg.(i+1))`1 = (pr1 fg).(i+1) & (fg.(i+1))`2 = (pr2 fg).(i+1)
    & (hi.(i+1))`1 = (pr1 hi).(i+1) & (hi.(i+1))`2 = (pr2 hi).(i+1)
    by FUNCT_2:def 5,def 6;
    (fg.i)`1 = (pr1 fg).i & (fg.i)`2 = (pr2 fg).i
    & (hi.i)`1 = (pr1 hi).i & (hi.i)`2 = (pr2 hi).i
    by FUNCT_2:def 5,def 6;
    hence thesis by A5,A6;
  end;

  EXLM1:for x,y be Element of INT
  holds
  ex g,w,q,t be sequence of INT,
  a,b,v,u be sequence of INT
  st
  a.0 = 1 & b.0 = 0 & g.0 = x & q.0=0
  & u.0 = 0 & v.0 = 1 & w.0 = y & t.0=0
  &
  (for i be Element of NAT
  holds
  q.(i+1) = g.i div w.i & t.(i+1) = g.i mod w.i
  &
  a.(i+1) = u.i & b.(i+1) = v.i & g.(i+1) = w.i
  &
  u.(i+1) = a.i - q.(i+1)*u.i & v.(i+1) = b.i - q.(i+1)*v.i
  &
  w.(i+1) = t.(i+1))
  proof
    let x,y be Element of INT;
    defpred P[Nat,Integer,Integer,Integer,Integer,
    Integer,Integer,Integer,Integer]
    means
    $6 = $4 div $5
    & $7 = $4 mod $5
    & $8 = $5
    & $9 = $7;

    A1: for n being Element of NAT,x being Element of INT,y being Element
    of INT,z being Element of INT,w being Element of INT
    ex x1 being Element of INT,y1 being Element of INT,
    z1 being Element of INT,w1 being Element of INT
    st P[n,x,y,z,w,x1,y1,z1,w1]
    proof
      let n be Element of NAT, x,y,z,w be Element of INT;
      reconsider x1 = z div w as Element of INT by INT_1:def 2;
      reconsider y1 = z mod w as Element of INT by INT_1:def 2;
      set z1 = w;
      set w1 = y1;
      take x1,y1,z1,w1;
      thus P[n,x,y,z,w,x1,y1,z1,w1];
    end;

    reconsider i1=1 as Element of INT by INT_1:def 2;
    reconsider i0=0 as Element of INT by INT_1:def 2;
    consider q,t,g,w be sequence of INT such that
    P1:
    q.0 = i0 & t.0 =i0 & g.0 = x & w.0 = y
    &
    for i be Element of NAT
    holds
    P[i,q.i,t.i,g.i,w.i,q.(i+1),t.(i+1),g.(i+1),w.(i+1)]
    from QuadChoiceRec(A1);

    defpred Q[Nat,Integer,Integer,Integer,Integer,
    Integer,Integer,Integer,Integer]
    means
    $6 = $4
    & $7 = $5
    & $8 = $2 - q.($1+1)*$4
    & $9 = $3 - q.($1+1)*$5;

    A2: for n being Element of NAT,
    x,y,z,w being Element of INT
    ex x1,y1,z1,w1 being Element of INT
    st Q[n,x,y,z,w,x1,y1,z1,w1]
    proof
      let n being Element of NAT,
      x,y,z,w being Element of INT;
      reconsider qn1=q.(n+1) as Element of INT;
      set x1 = z;
      set y1 = w;

      reconsider z1 = x- (q.(n+1))*z as Element of INT
      by INT_1:def 2;

      reconsider w1 = y- (q.(n+1))*w as Element of INT
      by INT_1:def 2;

      take x1,y1,z1,w1;
      thus Q[n,x,y,z,w,x1,y1,z1,w1];
    end;

    consider a,b,u,v be sequence of INT such that
    P2:
    a.0 = i1 & b.0 = i0 & u.0 = i0 & v.0 = i1
    &
    for i be Element of NAT holds

    Q[i,a.i,b.i,u.i,v.i,a.(i+1),b.(i+1),u.(i+1),v.(i+1)]
    from QuadChoiceRec(A2);
    take g,w,q,t,a,b,v,u;
    thus thesis by P1,P2;
  end;

  EXLM2:
  for x,y be Element of INT,
  g1,w1,q1,t1,
  a1,b1,v1,u1,
  g2,w2,q2,t2,
  a2,b2,v2,u2 be sequence of INT
  st
  ( a1.0 = 1 & b1.0 = 0 & g1.0 = x & q1.0=0
  & u1.0 = 0 & v1.0 = 1 & w1.0 = y & t1.0=0
  &
  (for i be Element of NAT
  holds
  q1.(i+1) = g1.i div w1.i & t1.(i+1) = g1.i mod w1.i
  &
  a1.(i+1) = u1.i & b1.(i+1) = v1.i & g1.(i+1) = w1.i
  &
  u1.(i+1) = a1.i - q1.(i+1)*u1.i & v1.(i+1)
  = b1.i - q1.(i+1)*v1.i
  &
  w1.(i+1) = t1.(i+1)) )
  &
  ( a2.0 = 1 & b2.0 = 0 & g2.0 = x & q2.0=0
  & u2.0 = 0 & v2.0 = 1 & w2.0 = y & t2.0=0
  &
  (for i be Element of NAT
  holds
  q2.(i+1) = g2.i div w2.i & t2.(i+1) = g2.i mod w2.i
  &
  a2.(i+1) = u2.i & b2.(i+1) = v2.i & g2.(i+1) = w2.i
  &
  u2.(i+1) = a2.i - q2.(i+1)*u2.i & v2.(i+1)
  = b2.i - q2.(i+1)*v2.i
  &
  w2.(i+1) = t2.(i+1)) )
  holds
  g1=g2 & w1 = w2 & q1 = q2 & t1 = t2
  & a1=a2 & b1 = b2 & v1 =v2 & u1 = u2

  proof
    let x,y be Element of INT,
    g1,w1,q1,t1,
    a1,b1,v1,u1,
    g2,w2,q2,t2,
    a2,b2,v2,u2 be sequence of INT;
    assume P1:
    ( a1.0 = 1 & b1.0 = 0 & g1.0 = x & q1.0=0
    & u1.0 = 0 & v1.0 = 1 & w1.0 = y & t1.0=0
    &
    (for i be Element of NAT
    holds
    q1.(i+1) = g1.i div w1.i & t1.(i+1) = g1.i mod w1.i
    &
    a1.(i+1) = u1.i & b1.(i+1) = v1.i & g1.(i+1) = w1.i
    &
    u1.(i+1) = a1.i - q1.(i+1)*u1.i & v1.(i+1) = b1.i - q1.(i+1)*v1.i
    &
    w1.(i+1) = t1.(i+1)) );
    assume P2:
    ( a2.0 = 1 & b2.0 = 0 & g2.0 = x & q2.0=0
    & u2.0 = 0 & v2.0 = 1 & w2.0 = y & t2.0=0
    &
    (for i be Element of NAT
    holds
    q2.(i+1) = g2.i div w2.i & t2.(i+1) = g2.i mod w2.i
    &
    a2.(i+1) = u2.i & b2.(i+1) = v2.i & g2.(i+1) = w2.i
    &
    u2.(i+1) = a2.i - q2.(i+1)*u2.i & v2.(i+1) = b2.i - q2.(i+1)*v2.i
    &
    w2.(i+1) = t2.(i+1)) );

    defpred P[Nat] means

    g1.$1 =g2.$1 & w1.$1 =w2.$1 & q1.$1 =q2.$1 & t1.$1 = t2.$1 &
    a1.$1 =a2.$1 & b1.$1 =b2.$1 & v1.$1 =v2.$1 & u1.$1 = u2.$1;

    P0: P[0] by P1,P2;
    PN: for n being Element of NAT st P[n] holds P[n+1]
    proof
      let n being Element of NAT;
      assume PN1:P[n];

      X1: q1.(n+1)
      =g2.n div w2.n by P1,PN1
      .= q2.(n+1) by P2;
      X2:t1.(n+1)
      = g2.n mod w2.n by P1,PN1
      .= t2.(n+1) by P2;
      X3:a1.(n+1)
      = u2.n by P1,PN1
      .= a2.(n+1) by P2;

      X4: b1.(n+1)
      = v2.n by PN1,P1
      .= b2.(n+1) by P2;
      X5: g1.(n+1)
      = w2.n by PN1,P1
      .= g2.(n+1) by P2;

      X6: u1.(n+1)
      = a2.n - q1.(n+1)*u2.n by P1,PN1
      .= u2.(n+1) by P2,X1;
      X7: v1.(n+1)
      = b2.n - q1.(n+1)*v2.n by PN1,P1
      .= v2.(n+1) by P2,X1;
      w1.(n+1)
      =t2.(n+1) by X2,P1
      .= w2.(n+1) by P2;

      hence P[n+1] by X1,X2,X3,X4,X5,X6,X7;
    end;

    for n being Element of NAT holds P[n] from NAT_1:sch 1(P0,PN);

    hence thesis by FUNCT_2:def 8;
  end;

definition
  let x,y be Element of INT;
  func ALGO_EXGCD(x,y) -> Element of [:INT,INT,INT:] means
  :defALGOEXGCD:
  ex g,w,q,t be sequence of INT,
  a,b,v,u be sequence of INT,
  istop be Element of NAT
  st
  a.0 = 1 & b.0 = 0 & g.0 = x & q.0 =0
  & u.0 = 0 & v.0 = 1 & w.0 = y & t.0 =0
  &
  (for i be Element of NAT
  holds
  q.(i+1) = g.i div w.i & t.(i+1) = g.i mod w.i
  &
  a.(i+1) = u.i & b.(i+1) = v.i & g.(i+1) = w.i
  &
  u.(i+1) = a.i - q.(i+1)*u.i & v.(i+1) = b.i - q.(i+1)*v.i
  &
  w.(i+1) = t.(i+1))
  & istop = min*{i where i is Element of NAT: w.i = 0}
  & (0 <= g.istop implies it =[a.istop,b.istop,g.istop] )
  & (g.istop < 0 implies it =[-(a.istop),-(b.istop),-(g.istop)] );
  existence
  proof
    consider g,w,q,t be sequence of INT,
    a,b,v,u be sequence of INT such that
    P1:
    a.0 = 1 & b.0 = 0 & g.0 = x & q.0=0
    & u.0 = 0 & v.0 = 1 & w.0 = y & t.0=0
    &
    (for i be Element of NAT
    holds
    q.(i+1) = g.i div w.i & t.(i+1) = g.i mod w.i
    &
    a.(i+1) = u.i & b.(i+1) = v.i & g.(i+1) = w.i
    &
    u.(i+1) = a.i - q.(i+1)*u.i & v.(i+1) = b.i - q.(i+1)*v.i
    &
    w.(i+1) = t.(i+1)) by EXLM1;

    set istop = min*{i where i is Element of NAT: w.i = 0};
    now per cases;
      suppose C1:0 <= g.istop;
        [a.istop,b.istop,g.istop] in [:INT,INT,INT:]
        by MCART_1:69;
        hence
        ex xx be Element of [:INT,INT,INT:]
        st
        (0 <= g.istop implies xx =[a.istop,b.istop,g.istop] )
        & (g.istop < 0 implies xx =[-(a.istop),-(b.istop),-(g.istop)] )
        by C1;
      end;
      suppose C2:g.istop < 0;

        X1: - g.istop in INT by INT_1:def 2;
        -a.istop in INT & -b.istop in INT by INT_1:def 2;
        then
        [-a.istop,-b.istop,-g.istop] in [:INT,INT,INT:]
        by MCART_1:69,X1;
        hence
        ex xx be Element of [:INT,INT,INT:]
        st
        (0 <= g.istop implies xx =[a.istop,b.istop,g.istop] )
        & (g.istop < 0 implies xx =[-(a.istop),-(b.istop),-(g.istop)] )
        by C2;
      end;
    end;
    then
    consider xx be Element of [:INT,INT,INT:] such that
    P2:
    (0 <= g.istop implies xx =[a.istop,b.istop,g.istop] )
    & (g.istop < 0 implies xx =[-(a.istop),-(b.istop),-(g.istop)] );
    take xx;

    thus thesis by P1,P2;
  end;

  uniqueness
  proof
    let s1,s2 be Element of [:INT,INT,INT:];

    assume A1:
    ex g1,w1,q1,t1,a1,b1,v1,u1 be sequence of INT,
    istop1 be Element of NAT
    st
    ( a1.0 = 1 & b1.0 = 0 & g1.0 = x & q1.0=0
    & u1.0 = 0 & v1.0 = 1 & w1.0 = y & t1.0=0
    &
    (for i be Element of NAT
    holds
    q1.(i+1) = g1.i div w1.i & t1.(i+1) = g1.i mod w1.i
    &
    a1.(i+1) = u1.i & b1.(i+1) = v1.i & g1.(i+1) = w1.i
    &
    u1.(i+1) = a1.i - q1.(i+1)*u1.i & v1.(i+1) = b1.i - q1.(i+1)*v1.i
    &
    w1.(i+1) = t1.(i+1)) )
    & istop1 = min*{i where i is Element of NAT: w1.i = 0}
    & (0 <= g1.istop1 implies s1 =[a1.istop1,b1.istop1,g1.istop1] )
    & (g1.istop1 < 0 implies s1 =[-(a1.istop1),-(b1.istop1),-(g1.istop1)] );

    assume
    A2:
    ex g2,w2,q2,t2 be sequence of INT,
    a2,b2,v2,u2 be sequence of INT,
    istop2 be Element of NAT
    st
    ( a2.0 = 1 & b2.0 = 0 & g2.0 = x & q2.0=0
    & u2.0 = 0 & v2.0 = 1 & w2.0 = y & t2.0=0
    &
    (for i be Element of NAT
    holds
    q2.(i+1) = g2.i div w2.i & t2.(i+1) = g2.i mod w2.i
    &
    a2.(i+1) = u2.i & b2.(i+1) = v2.i & g2.(i+1) = w2.i
    &
    u2.(i+1) = a2.i - q2.(i+1)*u2.i & v2.(i+1) = b2.i - q2.(i+1)*v2.i
    &
    w2.(i+1) = t2.(i+1)) )
    & istop2 = min*{i where i is Element of NAT: w2.i = 0}
    & (0 <= g2.istop2 implies s2 =[a2.istop2,b2.istop2,g2.istop2] )
    & (g2.istop2 < 0 implies s2 =[-(a2.istop2),-(b2.istop2),-(g2.istop2)] );

    consider
    g1,w1,q1,t1 be sequence of INT,
    a1,b1,v1,u1 be sequence of INT,
    istop1 be Element of NAT
    such that P1:
    ( a1.0 = 1 & b1.0 = 0 & g1.0 = x & q1.0=0
    & u1.0 = 0 & v1.0 = 1 & w1.0 = y & t1.0=0
    &
    (for i be Element of NAT
    holds
    q1.(i+1) = g1.i div w1.i & t1.(i+1) = g1.i mod w1.i
    &
    a1.(i+1) = u1.i & b1.(i+1) = v1.i & g1.(i+1) = w1.i
    &
    u1.(i+1) = a1.i - q1.(i+1)*u1.i & v1.(i+1)
    = b1.i - q1.(i+1)*v1.i
    &
    w1.(i+1) = t1.(i+1)) )
    & istop1 = min*{k where k is Element of NAT: w1.k = 0}
    & (0 <= g1.istop1 implies s1 =[a1.istop1,b1.istop1,g1.istop1] )
    & (g1.istop1 < 0 implies s1 =[-(a1.istop1),-(b1.istop1),-(g1.istop1)] )
    by A1;

    consider
    g2,w2,q2,t2 be sequence of INT,
    a2,b2,v2,u2 be sequence of INT,
    istop2 be Element of NAT
    such that P2:
    ( a2.0 = 1 & b2.0 = 0 & g2.0 = x & q2.0=0
    & u2.0 = 0 & v2.0 = 1 & w2.0 = y & t2.0=0
    &
    (for i be Element of NAT
    holds
    q2.(i+1) = g2.i div w2.i & t2.(i+1) = g2.i mod w2.i
    &
    a2.(i+1) = u2.i & b2.(i+1) = v2.i & g2.(i+1) = w2.i
    & u2.(i+1) = a2.i - q2.(i+1)*u2.i
    & v2.(i+1) = b2.i - q2.(i+1)*v2.i
    &
    w2.(i+1) = t2.(i+1)) )
    & istop2 = min*{k where k is Element of NAT: w2.k = 0}
    & (0 <= g2.istop2 implies s2 =[a2.istop2,b2.istop2,g2.istop2] )
    & (g2.istop2 < 0 implies s2 =[-(a2.istop2),-(b2.istop2),-(g2.istop2)] )
    by A2;

    g1=g2 & w1=w2 & a1=a2 & b1=b2 by P1,P2,EXLM2;
    hence s1=s2 by P1,P2;
  end;
end;

LM3G:for a,b be Element of INT,
A,B be sequence of INT
st
(A.0 = a & B.0 = b
&
(for i be Element of NAT
holds
A.(i+1) = B.i
&
B.(i+1) = A.i mod B.i))
holds
for i be Element of NAT
st B.i <> 0
holds
A.i gcd B.i = A.(i+1) gcd B.(i+1)
proof
  let a,b be Element of INT,
  A,B be sequence of INT;
  assume AS:
  A.0 = a & B.0 = b
  &
  (for i be Element of NAT
  holds
  A.(i+1) = B.i
  &
  B.(i+1) = A.i mod B.i);

  let i be Element of NAT;
  assume AS1: B.i <> 0;
  set k=A.i gcd B.i;

  Q1: A.(i+1) = B.i by AS;
  Q2: B.(i+1) = A.i mod B.i by AS;
  P1: k divides A.(i+1) by Q1,INT_2:def 2;
  P2: k divides B.(i+1)
  proof
    X1: B.(i+1) = A.i - (A.i div B.i ) * B.i by INT_1:def 10,Q2,AS1;
    X2: k divides A.i by INT_2:def 2;
    X3: k divides B.i by INT_2:def 2;

    X4:ex s being Integer
    st A.i = k*s by X2,INT_1:def 3;
    ex t being Integer
    st B.i = k*t by X3,INT_1:def 3;
    then
    consider s,t be Integer such that
    X5:B.(i+1) = (k*s) - (A.i div B.i ) * (k*t) by X1,X4;
    B.(i+1) = (s - (A.i div B.i)*t ) * k by X5;
    hence
    k divides B.(i+1) by INT_1:def 3;
  end;

  for m being Integer
  st m divides A.(i+1) & m divides B.(i+1) holds m divides k
  proof
    let m be Integer;
    assume P3: m divides A.(i+1) & m divides B.(i+1);
    then
    P31: m divides B.i by AS;
    P32: m divides A.i
    proof
      B.(i+1) = A.i - (A.i div B.i ) * B.i by INT_1:def 10,Q2,AS1;
      then
      X1: A.i = B.(i+1) + (A.i div B.i ) * B.i;

      X21:ex s being Integer
      st B.i = m * s by INT_1:def 3,P31;
      X22:ex t being Integer
      st B.(i+1) = m * t by INT_1:def 3,P3;
      consider s,t be Integer such that
      X4:A.i = (m*s) + (A.i div B.i ) * (m*t) by X1,X21,X22;
      A.i = m * (s + (A.i div B.i ) * t) by X4;
      hence m divides A.i by INT_1:def 3;
    end;

    thus m divides k by P31,P32,INT_2:def 2;
  end;
  hence
  A.(i+1) gcd B.(i+1) = k by P1,P2,INT_2:def 2;
end;

LM4G:for a,b be Element of INT,
A,B be sequence of INT
st
(A.0 = a & B.0 = b
&
(for i be Element of NAT
holds
A.(i+1) = B.i
&
B.(i+1) = A.i mod B.i))
holds
for i be Element of NAT st B.i <> 0
holds
A.0 gcd B.0 = A.i gcd B.i
proof
  let a,b be Element of INT,
  A,B be sequence of INT;
  assume AS1:
  A.0 = a & B.0 = b
  &
  (for i be Element of NAT
  holds
  A.(i+1) = B.i
  &
  B.(i+1) = A.i mod B.i);
  defpred P[Nat] means
  B.$1 <> 0 implies
  A.0 gcd B.0 = A.$1 gcd B.$1;

  P0: P[0];
  PN: for i being Element of NAT st P[i] holds P[i+1]
  proof
    let i being Element of NAT;
    assume PN1: P[i];
    B.(i+1) <> 0 implies
    A.0 gcd B.0 = A.(i+1) gcd B.(i+1)
    proof
      assume PN2: B.(i+1) <> 0;
      B.i <> 0
      proof
        assume PN4: B.i = 0;
        B.(i+1) = A.i mod B.i by AS1;
        hence contradiction by PN2,PN4,INT_1:def 10;
      end;
      hence thesis by PN1,AS1,LM3G;
    end;
    hence P[i+1];
  end;
  for i being Element of NAT holds P[i] from NAT_1:sch 1(P0,PN);
  hence thesis;
end;

theorem INT157A:
  for i2,i1 being Integer st i2 <= 0 holds
  i1 mod i2 <= 0
  proof
    let i2,i1 be Integer;
    assume A1: i2 <= 0;
    per cases by A1;
    suppose A2: i2 < 0;
      [\(i1 / i2)/] <= i1 / i2 by INT_1:def 6;
      then (i1 / i2) * i2 <= (i1 div i2) * i2
      by A2,XREAL_1:65;
      then i1 <= (i1 div i2) * i2 by A2,XCMPLX_1:87;
      then i1 - ((i1 div i2) * i2) <= 0 by XREAL_1:47;
      hence i1 mod i2 <= 0 by INT_1:def 10;
    end;
    suppose i2 = 0;
      hence i1 mod i2 <= 0 by INT_1:def 10;
    end;
  end;

theorem INT158A:
  for i2,i1 being Integer st i2 < 0 holds
  -(i1 mod i2) < -i2
  proof
    let i2,i1 be Integer;
    assume A1: i2 <0;
    (i1 / i2) - 1 < [\(i1 / i2)/] by INT_1:def 6;
    then (i1 div i2) * i2 < ((i1 / i2) - 1) * i2 by A1,XREAL_1:69;
    then (i1 div i2) * i2 < ((i1 / i2) * i2) - (1 * i2);
    then ((i1 div i2) * i2) < i1 - i2 by A1,XCMPLX_1:87;
    then ((i1 div i2) * i2) -i1 < i1 -i2 - i1 by XREAL_1:14;
    then -(i1- ((i1 div i2) * i2) ) < -i2;
    hence -( i1 mod i2) < -i2 by A1,INT_1:def 10;
  end;

theorem LM5G1:
  for x,y be Element of INT
  st abs(y) <> 0 holds
  abs(x mod y) < abs(y)
  proof
    let x,y be Element of INT;
    assume A1: abs(y) <> 0;
    per cases;
    suppose C1: 0 < y;
      then
      C2: x mod y < y by INT_1:58;
      0 <= x mod y by INT_1:57,C1;

      then
      C3: abs(x mod y) < y by ABSVALUE:def 1,C2;
      y <= abs(y) by ABSVALUE:4;
      hence abs(x mod y) < abs(y) by C3,XXREAL_0:2;
    end;
    suppose C4: y <= 0;
      C40P:y <> 0 by ABSVALUE:2,A1;

      C41: -(x mod y) < -y by INT158A,C40P,C4;
      XX1: (x mod y) <=0 by C4,INT157A;
      C42: abs(x mod y) = -(x mod y)
      proof
        per cases;
        suppose x mod y = 0;
          hence
          abs(x mod y) = -(x mod y) by ABSVALUE:2;
        end;
        suppose x mod y <> 0;
          hence
          abs(x mod y) = -(x mod y) by ABSVALUE:def 1,XX1;
        end;
      end;
      thus abs(x mod y) < abs(y) by C42,C41,C40P,C4,ABSVALUE:def 1;
    end;
  end;

  LM5G:for a,b be Element of INT,
  A,B be sequence of INT
  st
  (A.0 = a & B.0 = b
  &
  (for i be Element of NAT
  holds
  A.(i+1) = B.i
  &
  B.(i+1) = A.i mod B.i))
  holds
  {i where i is Element of NAT: B.i = 0}
  is non empty Subset of NAT
  proof
    let a,b be Element of INT,
    A,B be sequence of INT;
    assume AS1:
    A.0 = a & B.0 = b
    &
    (for i be Element of NAT
    holds
    A.(i+1) = B.i
    &
    B.(i+1) = A.i mod B.i);
    LMM: for x be set
    st x in
    {i where i is Element of NAT: B.i = 0}
    holds x in NAT
    proof let x be set;
      assume x in {i where i is Element of NAT: B.i = 0};
      then
      ex i be Element of NAT st x=i & B.i = 0;
      hence x in NAT;
    end;

    ex m0 be Element of NAT st B.m0 = 0
    proof
      assume A20:not (ex m0 be Element of NAT st B.m0 = 0);
      A2: for m0 be Element of NAT holds abs(B.m0) <> 0
      proof
        let m0 be Element of NAT;
        B.m0 <> 0 by A20;
        hence
        abs(B.m0) <> 0 by ABSVALUE:2;
      end;
      A3: for i be Element of NAT holds
      abs(B.(i+1)) <= abs(B.i) -1
      proof
        let i be Element of NAT;

        abs(B.(i+1)) = abs(A.i mod B.i) by AS1;
        then
        abs(B.(i+1)) < abs(B.i) by A2,LM5G1;
        then
        abs(B.(i+1)) +1 <= abs(B.i) by NAT_1:13;
        then
        abs(B.(i+1)) +1 -1 <= abs(B.i) -1 by XREAL_1:9;
        hence
        abs(B.(i+1)) <= abs(B.i) -1;
      end;
      defpred P[Nat] means abs(B.$1) <= abs(B.0) - $1;

      P0: P[0];
      P1:
      for i be Element of NAT st P[i] holds P[i+1]
      proof
        let i be Element of NAT;
        assume P11:P[i];
        P12: abs(B.(i+1)) <= abs(B.i) -1 by A3;
        abs(B.i) -1 <= (abs(B.0) - i) -1 by P11,XREAL_1:9;
        hence P[i+1] by XXREAL_0:2,P12;
      end;

      A4: for i be Element of NAT holds P[i] from NAT_1:sch 1(P0,P1);
      abs(B.abs(B.0)) <=abs(B.0) - abs((B.0)) by A4;
      hence contradiction by A2,NAT_1:14;
    end;
    then
    consider m0 be Element of NAT such that
    X1: B.m0 = 0;
    m0 in {i where i is Element of NAT: B.i = 0} by X1;
    hence thesis by LMM,TARSKI:def 3;
  end;

  LM6G: for a be Element of INT holds a gcd 0 = abs(a) by WSIERP_1:8;

  LM7G:
  for x,y be Element of INT,
  g,w,q,t be sequence of INT,
  a,b,v,u be sequence of INT
  st
  a.0 = 1 & b.0 = 0 & g.0 = x & q.0 =0
  & u.0 = 0 & v.0 = 1 & w.0 = y & t.0 =0
  &
  (for i be Element of NAT
  holds
  q.(i+1) = g.i div w.i & t.(i+1) = g.i mod w.i
  &
  a.(i+1) = u.i & b.(i+1) = v.i & g.(i+1) = w.i
  &
  u.(i+1) = a.i - q.(i+1)*u.i & v.(i+1) = b.i - q.(i+1)*v.i
  &
  w.(i+1) = t.(i+1))
  holds
  for i be Element of NAT
  st w.i <> 0
  holds
  a.(i+1) * x + b.(i+1) * y = g.(i+1)
  proof
    let x,y be Element of INT,
    g,w,q,t be sequence of INT,
    a,b,v,u be sequence of INT;
    assume AS:
    a.0 = 1 & b.0 = 0 & g.0 = x & q.0 =0
    & u.0 = 0 & v.0 = 1 & w.0 = y & t.0 =0
    &
    for i be Element of NAT
    holds
    q.(i+1) = g.i div w.i & t.(i+1) = g.i mod w.i
    &
    a.(i+1) = u.i & b.(i+1) = v.i & g.(i+1) = w.i
    &
    u.(i+1) = a.i - q.(i+1)*u.i & v.(i+1) = b.i - q.(i+1)*v.i
    &
    w.(i+1) = t.(i+1);

    defpred P[Nat] means
    w.$1 <> 0
    implies
    (a.($1) * x + b.($1) * y = g.($1)
    &
    a.($1+1) * x + b.($1+1) * y = g.($1+1));
    P0:P[0]
    proof
      assume w.0 <> 0;

      reconsider I0=0 as Element of NAT;

      a.(I0 + 1) *x + b.(I0 + 1)* y
      = (u.0)*x + b.(I0 + 1) *y by AS
      .= 0 *x + 1 *y by AS
      .= g.(I0 + 1) by AS;
      hence thesis by AS;
    end;

    P1: for i be Element of NAT
    st P[i] holds P[i+1]
    proof
      let i be Element of NAT;
      assume P12A: P[i];

      assume ASX: w.(i+1) <> 0;
      XX1: w.i <> 0
      proof
        assume
        XX2:w.i = 0;
        t.(i+1) = g.i mod w.i by AS
        .= 0 by XX2,INT_1:def 10;
        hence contradiction by AS,ASX;
      end;

      a.((i+1)+1) *x + b.((i+1)+1)* y
      = (u.(i+1))*x + b.((i+1)+1) *y by AS
      .= (u.(i+1))*x + (v.(i+1)) *y by AS
      .= (a.i - q.(i+1)*u.i)*x + (v.(i+1)) *y by AS
      .= (a.i - q.(i+1)*u.i)*x + (b.i - q.(i+1)*v.i) *y by AS
      .= g.i -q.(i+1)*(u.i*x + v.i*y ) by XX1,P12A
      .= g.i -q.(i+1)* (a.(i+1)*x + v.i*y) by AS
      .= g.i -q.(i+1)* g.(i+1) by XX1,P12A,AS
      .= g.i -(g.i div w.i)*g.(i+1) by AS
      .= g.i -(g.i div w.i)*w.i by AS
      .= g.i mod w.i by INT_1:def 10,XX1
      .= t.(i+1) by AS
      .= w.(i+1) by AS
      .= g.((i+1)+1) by AS;
      hence thesis by XX1,P12A;
    end;

    for i be Element of NAT holds P[i]
    from NAT_1:sch 1 (P0,P1);
    hence thesis;
  end;

theorem Th2:
  for x,y be Element of INT
  holds
  ALGO_EXGCD(x,y)`3_3 = x gcd y
  &
  ALGO_EXGCD(x,y)`1_3 * x + ALGO_EXGCD(x,y)`2_3 * y
  = x gcd y
  proof
    let x,y be Element of INT;
    consider g,w,q,t be sequence of INT,
    a,b,v,u be sequence of INT,
    istop be Element of NAT such that
    P0:
    a.0 = 1 & b.0 = 0 & g.0 = x & q.0 =0
    & u.0 = 0 & v.0 = 1 & w.0 = y & t.0 =0
    &
    (for i be Element of NAT
    holds
    q.(i+1) = g.i div w.i & t.(i+1) = g.i mod w.i
    &
    a.(i+1) = u.i & b.(i+1) = v.i & g.(i+1) = w.i
    &
    u.(i+1) = a.i - q.(i+1)*u.i & v.(i+1) = b.i - q.(i+1)*v.i
    &
    w.(i+1) = t.(i+1))
    & istop = min*{i where i is Element of NAT: w.i = 0}
    & (0 <= g.istop implies ALGO_EXGCD(x,y)
    =[a.istop,b.istop,g.istop] )
    & (g.istop < 0 implies ALGO_EXGCD(x,y)
    =[-(a.istop),-(b.istop),-(g.istop)] )
    by defALGOEXGCD;

    P2X:
    now let i be Element of NAT;
      thus g.(i+1) = w.i by P0;
      thus w.(i+1) = t.(i+1) by P0
      .= g.i mod w.i by P0;
    end;

    X0: {i where i is Element of NAT: w.i = 0}
    is non empty Subset of NAT by P0,P2X,LM5G;
    then
    istop in {i where i is Element of NAT: w.i = 0} by P0,NAT_1:def 1;
    then
    P4: ex i be Element of NAT st istop=i & w.i = 0;

    XX3: ALGO_EXGCD(x,y)`3_3 = abs(g.istop)
    proof
      per cases;
      suppose 0 <= g.istop;
        then
        abs(g.istop) = g.istop by ABSVALUE:def 1;
        hence
        ALGO_EXGCD(x,y)`3_3 = abs(g.istop) by P0,MCART_1:def 7;
      end;

      suppose XX32: g.istop < 0;
        then
        abs(g.istop) = -g.istop by ABSVALUE:def 1;
        hence
        ALGO_EXGCD(x,y)`3_3 = abs(g.istop) by P0,XX32,MCART_1:def 7;
      end;
    end;
    per cases;
    suppose C1:istop = 0;
      thus
      R1: ALGO_EXGCD(x,y)`3_3
      = x gcd y by P0,P4,LM6G,XX3,C1;

      thus
      ALGO_EXGCD(x,y)`1_3 * x + ALGO_EXGCD(x,y)`2_3 * y
      = x gcd y
      proof
        per cases;
        suppose Y11: 0 <= g.istop;

          Y13:ALGO_EXGCD(x,y)`1_3
          = 1 by C1,P0,Y11,MCART_1:def 5;

          ALGO_EXGCD(x,y)`2_3 = 0 by C1,P0,MCART_1:def 6;

          hence
          ALGO_EXGCD(x,y)`1_3 * x + ALGO_EXGCD(x,y)`2_3 * y
          = x gcd y by Y11,P0,C1,XX3,ABSVALUE:def 1,Y13,R1;
        end;

        suppose XX32: g.istop < 0;

          Y13:ALGO_EXGCD(x,y)`1_3 = -1 by C1,P0,XX32,MCART_1:def 5;

          ALGO_EXGCD(x,y)`2_3 = 0 by P0,C1,MCART_1:def 6;
          hence
          ALGO_EXGCD(x,y)`1_3 * x + ALGO_EXGCD(x,y)`2_3 * y
          = x gcd y by P0,C1,XX3,ABSVALUE:def 1,XX32,Y13,R1;
        end;
      end;
    end;

    suppose istop <> 0;
      then
      1 <= istop by NAT_1:14;
      then
      1-1 <= istop-1 by XREAL_1:9;
      then
      reconsider
      m1 = istop-1 as Element of NAT by INT_1:3;
      X1: w.m1 <> 0
      proof
        assume w.m1 = 0;
        then
        X11:m1 in {i where i is Element of NAT: w.i = 0};

        istop -1 < istop - 0 by XREAL_1:15;
        hence contradiction by X11,P0,X0,NAT_1:def 1;
      end;

      P5: g.m1 gcd w.m1 = g.(m1+1) gcd w.(m1+1) by LM3G,P0,X1,P2X;

      R1: g.(istop) gcd w.(istop)
      = ALGO_EXGCD(x,y)`3_3 by XX3,LM6G,P4;
      hence
      RR1:ALGO_EXGCD(x,y)`3_3 = x gcd y by P5,X1,P2X,LM4G,P0;

      Y1:a.(m1+1) * x + b.(m1+1) * y = g.(m1+1)
      by X1,LM7G,P0;

      thus
      ALGO_EXGCD(x,y)`1_3 * x + ALGO_EXGCD(x,y)`2_3 * y
      = x gcd y
      proof
        per cases;
        suppose Y11: 0 <= g.istop;
          then
          Y12:ALGO_EXGCD(x,y)`3_3 = g.istop by XX3,ABSVALUE:def 1;

          ALGO_EXGCD(x,y)`1_3 = a.(istop) by P0,Y11,MCART_1:def 5;
          hence
          ALGO_EXGCD(x,y)`1_3 * x + ALGO_EXGCD(x,y)`2_3 * y
          = x gcd y by RR1,Y1,Y12,P0,MCART_1:def 6;
        end;

        suppose XX32: g.istop < 0;
          then
          Y12:ALGO_EXGCD(x,y)`3_3 = -g.istop by XX3,ABSVALUE:def 1;
          Y13:ALGO_EXGCD(x,y)`1_3 = -a.(istop) by P0,XX32,MCART_1:def 5;

          ALGO_EXGCD(x,y)`2_3 = -b.(istop) by P0,XX32,MCART_1:def 6;

          hence
          ALGO_EXGCD(x,y)`1_3 * x + ALGO_EXGCD(x,y)`2_3 * y
          = x gcd y by Y1,Y12,Y13,R1,P5,X1,P2X,LM4G,P0;
        end;
      end;
    end;
  end;

::==========================================================================================
::NZMATH source code
:: def inverse(x,p):
:: """
:: This function returns inverse of x for modulo p.
:: """
:: x = x % p
:: y = gcd.extgcd(p,x)
:: if y[2] == 1:
:: if y[1] < 0:
:: r = p + y[1]
:: return r
:: else:
:: return y[1]
:: raise ZeroDivisionError("There is no inverse for %d modulo %d." % (x,p))
::=======================================================================================

definition
  let x,p be Element of INT;
  func ALGO_INVERSE(x,p) -> Element of INT means
  :definverse:
  for y be Element of INT st y = (x mod p) holds
  ( ALGO_EXGCD(p,y)`3_3 = 1 implies
  ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
  (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
  & it = p + z ))
  &
  ( (0 <= ALGO_EXGCD(p,y)`2_3) implies it = ALGO_EXGCD(p,y)`2_3)
  )
  &
  ( ALGO_EXGCD(p,y)`3_3 <> 1 implies it = {} );
  existence
  proof
    reconsider y = x mod p as Element of INT by INT_1:def 2;
    now per cases;
      suppose C1: ALGO_EXGCD(p,y)`3_3 = 1;
        now per cases;
          suppose C11: ( ALGO_EXGCD(p,y)`2_3 < 0);

            reconsider z = ALGO_EXGCD(p,y)`2_3
            as Element of INT;
            reconsider s = p + z
            as Element of INT by INT_1:def 2;
            ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
            & s = p + z;
            hence ex s be Element of INT st
            ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
            (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
            & s = p + z ) )
            &
            ( (0 <= ALGO_EXGCD(p,y)`2_3) implies s = ALGO_EXGCD(p,y)`2_3 )
            &
            ( ALGO_EXGCD(p,y)`3_3 <> 1 implies s = {} )
            by C11,C1;
          end;
          suppose C12: ( 0 <= ALGO_EXGCD(p,y)`2_3 );
            reconsider s = ALGO_EXGCD(p,y)`2_3
            as Element of INT;

            thus ex s be Element of INT st
            ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
            (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
            & s = p + z ) )
            &
            ( (0 <= ALGO_EXGCD(p,y)`2_3) implies s = ALGO_EXGCD(p,y)`2_3 )
            &
            ( ALGO_EXGCD(p,y)`3_3 <> 1 implies s = {} )
            by C12,C1;
          end;
        end;
        hence
        ex s be Element of INT st
        ( ALGO_EXGCD(p,y)`3_3 = 1 implies
        ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
        (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
        & s = p + z ))
        &
        ( (0 <= ALGO_EXGCD(p,y)`2_3) implies s = ALGO_EXGCD(p,y)`2_3)
        )
        &
        ( ALGO_EXGCD(p,y)`3_3 <> 1 implies s = {} );
      end;
      suppose C2: ALGO_EXGCD(p,y)`3_3 <> 1;
        reconsider s ={} as Element of INT by INT_1:def 2;
        ALGO_EXGCD(p,y)`3_3 <> 1 implies s = {};
        hence
        ex s be Element of INT st
        ( ALGO_EXGCD(p,y)`3_3 = 1 implies
        ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
        (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
        & s = p + z ))
        &
        ( (0 <= ALGO_EXGCD(p,y)`2_3) implies s = ALGO_EXGCD(p,y)`2_3)
        )
        &
        ( ALGO_EXGCD(p,y)`3_3 <> 1 implies s = {} ) by C2;
      end;
    end;
    then
    consider s be Element of INT such that
    Q1:
    ( ALGO_EXGCD(p,y)`3_3 = 1 implies
    ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
    (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
    & s = p + z ))
    &
    ( (0 <= ALGO_EXGCD(p,y)`2_3) implies s = ALGO_EXGCD(p,y)`2_3)
    )
    &
    ( ALGO_EXGCD(p,y)`3_3 <> 1 implies s = {} );
    take s;
    thus
    for y be Element of INT
    st y = (x mod p)
    holds
    ( ALGO_EXGCD(p,y)`3_3 = 1 implies
    ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
    (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
    & s = p + z ))
    &
    ( (0 <= ALGO_EXGCD(p,y)`2_3) implies s = ALGO_EXGCD(p,y)`2_3)
    )
    &
    ( ALGO_EXGCD(p,y)`3_3 <> 1 implies s = {} ) by Q1;
  end;
  uniqueness
  proof
    let s1,s2 be Element of INT;
    assume A1:
    for y be Element of INT st y = (x mod p) holds
    ( ALGO_EXGCD(p,y)`3_3 = 1 implies
    ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
    (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3 & s1 = p + z )) &
    ( (0 <= ALGO_EXGCD(p,y)`2_3) implies s1 = ALGO_EXGCD(p,y)`2_3)) &
    ( ALGO_EXGCD(p,y)`3_3 <> 1 implies s1 = {} );
    assume A2:
    for y be Element of INT st y = (x mod p) holds
    ( ALGO_EXGCD(p,y)`3_3 = 1 implies
    ( ( ALGO_EXGCD(p,y)`2_3 < 0) implies
    (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3 & s2 = p + z ))
    &
    ( (0 <= ALGO_EXGCD(p,y)`2_3) implies s2 = ALGO_EXGCD(p,y)`2_3)
    )
    &
    ( ALGO_EXGCD(p,y)`3_3 <> 1 implies s2 = {} );
    reconsider y = x mod p as Element of INT by INT_1:def 2;
    thus s1=s2
    proof
      per cases;
      suppose C1: ALGO_EXGCD(p,y)`3_3 = 1;
        thus s1=s2
        proof
          per cases;
          suppose C11: ALGO_EXGCD(p,y)`2_3 < 0;
            then
            C12: (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
            & s1 = p + z ) by A1,C1;
            (ex z be Element of INT st z = ALGO_EXGCD(p,y)`2_3
            & s2 = p + z ) by A2,C1,C11;
            hence s1=s2 by C12;
          end;
          suppose C12: 0 <= ALGO_EXGCD(p,y)`2_3;
            thus
            s1 = ALGO_EXGCD(p,y)`2_3 by C12,C1,A1
            .=s2 by C12,C1,A2;
          end;
        end;
      end;
      suppose C2: ALGO_EXGCD(p,y)`3_3 <> 1;
        thus s1= {} by A1,C2
        .= s2 by A2,C2;
      end;
    end;
  end;
end;

  LMTh30:
  for x,y,p be Element of INT
  st y = x mod p & ALGO_EXGCD(p,y)`3_3 = 1 & p <> 0
  holds
  ( ALGO_INVERSE(x,p) * x ) mod p = 1 mod p
  proof
    let x,y,p be Element of INT;
    assume AS: y = x mod p & ALGO_EXGCD(p,y)`3_3 = 1 & p <> 0;
    P3P:ALGO_EXGCD(p,y)`3_3 = p gcd y &
    ALGO_EXGCD(p,y)`1_3 * p + ALGO_EXGCD(p,y)`2_3 * y
    = p gcd y by Th2;

    reconsider s1 = ALGO_EXGCD(p,y)`1_3 * p as Integer;
    reconsider s2 = (ALGO_EXGCD(p,y))`2_3 * y as Integer;
    reconsider s3 = (ALGO_EXGCD(p,y))`2_3 as Integer;

    P40C2:(p mod p)=0 by INT_1:50;

    P4: ( ALGO_EXGCD(p,y)`1_3 * p ) mod p
    = (( ALGO_EXGCD(p,y)`1_3 mod p ) * (p mod p)) mod p by NAT_D:67
    .= 0 by INT_4:12,P40C2;

    reconsider I0 = 0 as Element of INT by INT_1:def 2;

    P6: (ALGO_EXGCD(p,y)`1_3 * p + ALGO_EXGCD(p,y)`2_3 * y )
    mod p
    = ((s1 mod p) + (s2 mod p)) mod p
    by NAT_D:66
    .= ( ALGO_EXGCD(p,y)`2_3 * y ) mod p by LMTh3,P4;

    per cases;
    suppose ALGO_EXGCD(p,y)`2_3 < 0;
      then
      consider z be Element of INT such that
      A11: z = ALGO_EXGCD(p,y)`2_3
      & ALGO_INVERSE(x,p) = p + z by definverse,AS;
      thus ( ALGO_INVERSE(x,p) * x ) mod p
      =( p*x + z*x ) mod p by A11
      .= (z*x) mod p by NAT_D:61
      .= ((z mod p) *(x mod p)) mod p by NAT_D:67
      .= ((z mod p) *((x mod p) mod p) ) mod p by LMTh3
      .= 1 mod p by P6,A11,P3P,AS,NAT_D:67;
    end;
    suppose
      0 <= ALGO_EXGCD(p,y)`2_3;
      hence
      ( ALGO_INVERSE(x,p) * x ) mod p
      = ((ALGO_EXGCD(p,y)`2_3)*x ) mod p by definverse,AS
      .= ((s3 mod p) * (x mod p) ) mod p by NAT_D:67
      .= ( (s3 mod p) * ((x mod p) mod p) ) mod p
      by LMTh3
      .= 1 mod p by P6,P3P,AS,NAT_D:67;
    end;
  end;

theorem Th3:
  for x,p,y be Element of INT
  st y = x mod p & ALGO_EXGCD(p,y)`3_3 = 1
  holds
  ( ALGO_INVERSE(x,p) * x ) mod p = 1 mod p
  proof
    let x,p,y be Element of INT;
    assume AS: y = x mod p & ALGO_EXGCD(p,y)`3_3 = 1;
    per cases;
    suppose C1: p = 0;
      thus ( ALGO_INVERSE(x,p) * x ) mod p = 0 by C1,INT_1:def 10
      .= 1 mod p by C1,INT_1:def 10;
    end;
    suppose p <> 0;
      hence ( ALGO_INVERSE(x,p) * x ) mod p = 1 mod p by LMTh30,AS;
    end;
  end;

begin ::Algorithm for Chinese Remainder Theorem
:: def ALGO_CRT(nlist):
:: """
:: This function is Chinese Remainder Theorem using Algorithm 2.1.7
:: of C.Pomerance and R.Crandall's book.
::
:: For example:
:: >>> ALGO_CRT([(1,2),(2,3),(3,5)])
:: 23
:: """
:: r = len(nlist)
:: if r == 1 :
:: return nlist [ 0 ] [ 0 ]
::
:: product = []
:: prodinv = []
:: m = 1
:: for i in range(1,r):
:: m = m*nlist[i-1][1]
:: c = inverse(m,nlist[i][1])
:: product.append(m)
:: prodinv.append(c)
::
:: M = product[r-2]*nlist[r-1][1]
:: n = nlist[0][0]
:: for i in range(1,r):
:: u = ((nlist[i][0]-n)*prodinv[i-1]) % nlist[i][1]
:: n += u*product[i-1]
:: return n % M
::==========================================================================================

definition
  let nlist be non empty FinSequence of [:INT,INT:];
  func ALGO_CRT(nlist) -> Element of INT means
  :defALGOCRT:
  ( len nlist = 1 implies it = (nlist.1)`1)
  &
  ( len nlist <> 1 implies
  ex m,n,prodc,prodi be FinSequence of INT,
  M0,M be 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 be Nat
  st 1<=i & i<=(len m) - 1
  holds
  ex d,x,y be 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 be Nat st 1<=i & i<=len m - 1 holds
  ex u,u0,u1 be 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)) &
  it = n.(len m) mod M );
  existence
  proof
    per cases;
    suppose A1: len nlist = 1;
      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 thesis by A1;
    end;
    suppose A2: len nlist <> 1;
      defpred P[Nat,Integer,Integer] means
      ex x be 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)
      for z being Element of INT ex y being Element of INT st P[n,z,y]
      proof
        let n being Element of NAT;
        assume X11: 1 <= n & n < len nlist;
        let z being Element of INT;
        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;
        thus P[n,z,y];
      end;

      consider m being FinSequence of INT such that
      X2: len m = len nlist & (m.1 = i1 or len nlist = 0) &
      for i be Element of NAT st 1 <= i & i < len nlist
      holds P[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 be Nat
      st 1<=i & i<=(len m) -1
      holds ex x be Element of INT
      st x = (nlist.i)`2
      &
      m.(i+1) = m.i * x
      proof
        let i be Nat;
        assume 1<=i & i<=(len m) -1;
        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 be Element of INT
        st x = (nlist.i)`2 &
        m.(i+1) = m.i * x by X2,X32;
      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 P1[Nat,Integer] means
      ex d,x,y be 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
      ex z being Element of INT st P1[n,z]
      proof
        let n be Nat;
        assume X41: n in Seg lm;
        X43: 1 <= n & n <= (len m) - 1 by FINSEQ_1:1,X41;
        then
        consider x be 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;
        thus P1[n,w] by X42;
      end;

      consider prodi being FinSequence of INT such that
      X5: dom prodi = Seg lm &
      for k be Nat st k in Seg lm holds P1[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 be Nat
      st 1<=i & i<=(len m) -1
      holds ex d,x,y be 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;
        assume 1<=i & i<=(len m) -1;
        then
        i in Seg(lm) by FINSEQ_1:1;
        hence ex d,x,y be 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;
      end;

      defpred P2[Nat,Integer] means
      ex d,x,y be 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
      ex z being Element of INT st P2[n,z]
      proof
        let n be Nat;
        assume X41: n in Seg lm;
        1 <= n & n <= (len m) - 1 by FINSEQ_1:1,X41;
        then
        consider d,x,y be 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;
        thus P2[n,w] by X42;
      end;

      consider prodc being FinSequence of INT such that
      X9: dom prodc = Seg lm &
      for k be Nat st k in Seg lm holds P2[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 be Nat
      st 1<=i & i<=(len m) -1
      holds ex d,x,y be 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;
        assume 1<=i & i<=(len m) -1;
        then
        i in Seg(lm) by FINSEQ_1:1;
        hence
        ex d,x,y be 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 X9;
      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 P4[Nat,Integer,Integer ] means
      ex u,u0,u1 be 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)
      for z being Element
      of INT ex y being Element of INT st P4[n,z,y]
      proof
        let n being Element of NAT;
        assume X41: 1 <= n & n < len nlist;

        let z being Element of INT;

        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;
        thus P4[n,z,y];
      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 be Element of NAT st 1 <= i & i < len nlist
      holds P4[i,n.i,n.(i+1)] from RECDEF_1:sch 4(X12);

      X14:for i be Nat
      st 1<=i & i<=(len m) -1
      holds
      ex u,u0,u1 be 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;
        assume 1<=i & i<=(len m) -1;
        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 be 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;
      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 thesis by A2,X14,X11,X2,X13,X6,X10;
    end;
  end;
  uniqueness
  proof
    let s1,s2 be Element of INT;
    assume
    A1:
    ( len nlist = 1 implies s1 = (nlist.1)`1)
    &
    ( len nlist <> 1 implies
    ex m,n,prodc,prodi be FinSequence of INT,
    M0,M be 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 be Nat st 1<=i & i<=(len m) -1 holds
    ex d,x,y be 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 be Nat
    st 1<=i & i<=len m -1
    holds
    ex u,u0,u1 be 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))&
    s1 = n.(len m) mod M );

    assume
    A2:
    ( len nlist = 1 implies s2 = (nlist.1)`1)
    &
    ( len nlist <> 1 implies
    ex m,n,prodc,prodi be FinSequence of INT,
    M0,M be 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 be Nat
    st 1<=i & i<=(len m) -1
    holds
    ex d,x,y be 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 be Nat
    st 1<=i & i<=len m -1
    holds
    ex u,u0,u1 be 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) ) &
    s2 = n.(len m) mod M );

    per cases;
    suppose C1: len nlist = 1;
      thus s1 = s2 by A1,A2,C1;
    end;
    suppose C2: len nlist <> 1;

      consider m1,n1,prodc1,prodi1 be FinSequence of INT,
      M01,M1 be Element of INT such that
      P1: len m1 = len nlist
      & len n1 = len nlist
      & len prodc1 = len nlist -1
      & len prodi1 = len nlist -1
      & m1.1 =1
      & (for i be Nat
      st 1<=i & i<=(len m1) -1
      holds
      ex d,x,y be Element of INT st x = (nlist.i)`2
      &
      m1.(i+1) = m1.i * x
      &
      y = m1.(i+1)
      &
      d = (nlist.(i+1))`2
      &
      prodi1.i = ALGO_INVERSE(y,d)
      &
      prodc1.i = y
      )
      & M01 = (nlist.(len m1))`2
      & M1 = (prodc1.((len m1)-1))*M01
      & n1.1 = (nlist.1)`1
      & (for i be Nat
      st 1<=i & i<=len m1 -1
      holds
      ex u,u0,u1 be Element of INT
      st
      u0 = ( nlist.(i+1))`1
      &
      u1 = ( nlist.(i+1))`2
      &
      u = ( (u0- n1.i)*(prodi1.i)) mod u1
      & n1.(i+1) = n1.i + u*(prodc1.i) )
      & s1 = n1.(len m1) mod M1 by C2,A1;

      consider m2,n2,prodc2,prodi2 be FinSequence of INT,
      M02,M2 be Element of INT such that
      P2: len m2 = len nlist
      & len n2 = len nlist
      & len prodc2 = len nlist -1
      & len prodi2 = len nlist -1
      & m2.1 =1
      & (for i be Nat
      st 1<=i & i<=(len m2) -1
      holds
      ex d,x,y be Element of INT
      st x = (nlist.i)`2
      &
      m2.(i+1) = m2.i * x
      &
      y = m2.(i+1)
      &
      d = (nlist.(i+1))`2
      &
      prodi2.i = ALGO_INVERSE(y,d)
      &
      prodc2.i = y
      )
      & M02 = (nlist.(len m2))`2
      & M2 = (prodc2.((len m2)-1))*M02
      & n2.1 = (nlist.1)`1
      & (for i be Nat
      st 1<=i & i<=len m2 -1
      holds
      ex u,u0,u1 be Element of INT
      st
      u0 = ( nlist.(i+1))`1
      &
      u1 = ( nlist.(i+1))`2
      &
      u = ( (u0- n2.i)*(prodi2.i)) mod u1
      & n2.(i+1) = n2.i + u*(prodc2.i) )
      & s2 = n2.(len m2) mod M2 by C2,A2;
      defpred EQ[Nat] means
      1<= $1 & $1 <= len m1
      implies m1.$1 =m2.$1;
      Q50:EQ[ 0 ];

      Q51: for i be Nat
      st EQ[i] holds EQ[i+1]
      proof
        let i be Nat;
        assume Q52: EQ[i];
        assume
        1<= i+1 & i+1 <= len m1;
        then
        Q54:1-1 <=i+1 -1 & i+1 -1 <= len m1 -1 by XREAL_1:9;

        Q55:len m1 -1 <= len m1 - 0 by XREAL_1:13;

        per cases;
        suppose C1: i = 0;
          thus
          m1.(i+1) = m2.(i+1) by P1,P2,C1;
        end;
        suppose Q56P:i <> 0;
          then
          Q56: 1<=i by NAT_1:14;

          Q57: ex d,x,y be Element of INT
          st x = (nlist.i)`2 &
          m1.(i+1) = m1.i * x &
          y = m1.(i+1) &
          d = (nlist.(i+1))`2 &
          prodi1.i = ALGO_INVERSE(y,d) &
          prodc1.i = y by P1,Q56,Q54;

          1<=i & i<=len m2 -1 by Q56P,Q54,P1,P2,NAT_1:14;
          then ex d,x,y be Element of INT
          st x = (nlist.i)`2 &
          m2.(i+1) = m2.i * x &
          y = m2.(i+1) &
          d = (nlist.(i+1))`2 &
          prodi2.i = ALGO_INVERSE(y,d) &
          prodc2.i = y by P2;
          hence
          m1.(i+1) = m2.(i+1) by Q57,Q54,Q52,Q55,Q56P,NAT_1:14,XXREAL_0:2;
        end;
      end;

      Q0:for k be Nat holds EQ[k]
      from NAT_1:sch 2(Q50,Q51);

      QQ3: now let i be Nat;
      assume ASX0:1<=i & i <=len prodc1;
      then
      X1: ex d,x,y be Element of INT
      st x = (nlist.i)`2 &
      m1.(i+1) = m1.i * x &
      y = m1.(i+1) &
      d = (nlist.(i+1))`2 &
      prodi1.i = ALGO_INVERSE(y,d) &
      prodc1.i = y by P1;

      ex d,x,y be Element of INT
      st x = (nlist.i)`2 &
      m2.(i+1) = m2.i * x &
      y = m2.(i+1) &
      d = (nlist.(i+1))`2 &
      prodi2.i = ALGO_INVERSE(y,d) &
      prodc2.i = y by P2,ASX0,P1;
      hence
      prodc1.i = prodc2.i by X1,FINSEQ_1:14,P1,P2,Q0;
    end;
    then
    Q3: prodc1 = prodc2 by FINSEQ_1:14,P1,P2;
    Q3A:now let i be Nat;
    assume ASX0:1<=i & i <=len prodi1;
    then
    X1: ex d,x,y be Element of INT
    st x = (nlist.i)`2 &
    m1.(i+1) = m1.i * x &
    y = m1.(i+1) &
    d = (nlist.(i+1))`2 &
    prodi1.i = ALGO_INVERSE(y,d) &
    prodc1.i = y by P1;

    ex d,x,y be Element of INT
    st x = (nlist.i)`2 &
    m2.(i+1) = m2.i * x &
    y = m2.(i+1) &
    d = (nlist.(i+1))`2 &
    prodi2.i = ALGO_INVERSE(y,d) &
    prodc2.i = y by P2,ASX0,P1;
    hence
    prodi1.i = prodi2.i by X1,Q0,FINSEQ_1:14,P1,P2;
  end;

  Q4: M1 = M2 by P2,FINSEQ_1:14,P1,QQ3;

  defpred EQ[Nat] means
  1<= $1 & $1 <= len n1
  implies n1.$1 =n2.$1;
  Q50:EQ[ 0 ];

  Q51: for k be Nat
  st EQ[k] holds EQ[k+1]
  proof
    let k be Nat;
    assume Q52: EQ[k];
    assume 1<= k+1 & k+1 <= len n1;
    then
    Q54:1-1 <=k+1 -1 & k+1 -1 <= len n1 -1 by XREAL_1:9;

    Q55:len n1 -1 <= len n1 - 0 by XREAL_1:13;

    per cases;
    suppose C1: k = 0;
      thus
      n1.(k+1) = n2.(k+1) by P1,P2,C1;
    end;
    suppose ASQ56:k <> 0;
      then
      Q56: 1<=k by NAT_1:14;

      Q57: ex u,u0,u1 be Element of INT
      st
      u0 = ( nlist.(k+1))`1
      &
      u1 = ( nlist.(k+1))`2
      &
      u = ((u0- n1.k)*(prodi1.k)) mod u1
      &
      n1.(k+1) = n1.k + u*(prodc1.k) by Q56,Q54,P1;

      ex u,u0,u1 be Element of INT
      st
      u0 = ( nlist.(k+1))`1
      &
      u1 = ( nlist.(k+1))`2
      &
      u = ( (u0- n2.k)*(prodi2.k)) mod u1
      &
      n2.(k+1) = n2.k + u*(prodc2.k) by Q56,Q54,P1,P2;
      hence
      n1.(k+1) = n2.(k+1) by Q3,Q57,Q52,Q55,ASQ56,
      NAT_1:14,Q54,XXREAL_0:2,FINSEQ_1:14,P1,P2,Q3A;
    end;
  end;

  for k be Nat holds EQ[k] from NAT_1:sch 2(Q50,Q51);
  hence s1=s2 by Q4,P1,P2,FINSEQ_1:14;
end;
end;
end;

theorem LMLmTh4B:
  for a,b be Element of INT st b <> 0 holds (a mod b),a are_congruent_mod b
  proof
    let a,b be Element of INT;
    assume b <>0;then
    C1:a mod b = a - (a div b) * b by INT_1:def 10;
    reconsider c = -(a div b) as Element of INT by INT_1:def 2;
    take c;
    thus thesis by C1;
  end;

theorem
  for a,b be Element of INT st b <>0 holds
  (a mod b ) gcd b = a gcd b by INT_4:14,LMLmTh4B;

theorem LmTh4A:
  for a,b,c be Element of INT
  st c <>0 & a = b mod c
  &
  b,c are_relative_prime
  holds a,c are_relative_prime
  proof
    let a,b,c be Element of INT;
    assume A1: c <>0 &
    a = b mod c
    &
    b,c are_relative_prime;
    then
    b gcd c = 1 by INT_2:def 3;
    then
    a gcd c = 1 by A1,INT_4:14,LMLmTh4B;
    hence thesis by INT_2:def 3;
  end;

  LmTh4:
  for a,b,c be Element of INT
  st a = b mod c & c <> 0 holds
  ex d be Element of INT st a = b + d * c
  proof
    let a,b,c be Element of INT;
    assume a = b mod c & c <> 0;then
    C1:b = (b div c)*c + a by INT_1:59;
    reconsider x = -(b div c) as Element of INT by INT_1:def 2;
    take x;
    thus thesis by C1;
  end;

  LmTh5A:
  for b,m be FinSequence of INT
  st len b = len m
  &
  (for i be Nat st i in Seg (len b)
  holds b.i <> 0 )
  &
  m.1 = 1
  holds
  for k be Element of NAT
  st
  1<= k & k <= len b -1
  &
  (for i be Nat st 1<=i & i <=k
  holds
  m.(i+1) = m.i * b.i )
  holds
  m.(k+1) <> 0
  proof
    let b,m be FinSequence of INT;
    assume len b = len m;
    assume A2: (for i be Nat st i in Seg (len b)
    holds b.i <> 0 )&
    m.1 = 1;

    defpred P[Nat] means
    ( 1<= $1 & $1 <= len b -1
    &
    (for i be Nat st
    1<=i & i <=$1
    holds
    m.(i+1) = m.i * b.i ) )
    implies
    m.($1+1) <> 0;
    reconsider I0=0 as Element of NAT;
    P0:P[0];

    P1:for k be Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT;
      assume P11: P[k];
      assume P12:
      1<= k+1 & k+1 <= len b -1
      &
      (for i be Nat st
      1<=i & i <=k+1
      holds
      m.(i+1) = m.i * b.i );

      P14: k <= k +1 by NAT_1:12;
      per cases;
      suppose P15: k = 0;
        P16: m.((k+1)+1)
        = m.1 * b.1 by P12,P15
        .= b.1 by A2;

        len b -1 + (0 qua Nat) <= len b - 1 + 1 by XREAL_1:7;
        then
        k+1 <= len b by P12,XXREAL_0:2;
        then
        1 <= 1 & 1 <= len b by XXREAL_0:2,P12;
        then
        1 in Seg(len b);
        hence
        m.((k+1)+1) <> 0 by P16,A2;
      end;
      suppose P19:k <> 0;

        P20: now let i be Nat;
        assume 1<=i & i <=k;
        then
        1<=i & i <=(k +1) by NAT_1:12;
        hence
        m.(i+1) = m.i * b.i by P12;
      end;

      thus
      m.((k+1)+1) <> 0
      proof
        XX6:(k+1) +1 <= len b -1 +1 by P12,XREAL_1:6;

        XX1: (k +1) <= (k+1) +1 by NAT_1:12;

        XX2: 1<= k+1 by NAT_1:12;
        k +1 <= len b by XX1,XX6,XXREAL_0:2;
        then
        k+1 in Seg (len b) by XX2;
        then
        P23:
        b.(k+1) <> 0 by A2;
        m.((k+1)+1) = m.(k+1) * b.(k+1) by P12;
        hence
        m.((k+1)+1) <> 0 by P23,P20,P11,P12,P14,
        XXREAL_0:2,NAT_1:14,P19,XCMPLX_1:6;
      end;
    end;
  end;
  for k be Element of NAT holds P[k] from NAT_1:sch 1(P0,P1);
  hence thesis;
end;

LmTh5:
for b,m be FinSequence of INT
st 2 <=len b
&
(for i,j be Nat st i in Seg (len b)
& j in Seg (len b)
& i <> j
holds b.i,b.j are_relative_prime )
&
m.1 = 1
holds
for k be Element of NAT
st
1<= k & k <= len b -1
&
(for i be Nat st 1<=i & i <=k
holds
m.(i+1) = m.i * b.i )
holds
for j be Nat st k+1 <= j & j <= len b
holds
m.(k+1),b.j are_relative_prime
proof
  let b,m be FinSequence of INT;
  assume 2 <=len b;
  assume
  A2: (for i,j be Nat st i in Seg (len b)
  & j in Seg (len b)
  & i <> j
  holds b.i,b.j are_relative_prime )
  &
  m.1 = 1;
  defpred P[Nat] means
  ( 1<= $1 & $1 <= len b -1
  &
  (for i be Nat st
  1<=i & i <=$1
  holds
  m.(i+1) = m.i * b.i ) )
  implies
  for j be Nat st $1+1 <= j & j <= len b
  holds
  m.($1+1),b.j are_relative_prime;
  reconsider I0=0 as Element of NAT;
  P0:P[0];

  P1:for k be Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of NAT;
    assume P11: P[k];
    assume P12:
    1<= k+1 & k+1 <= len b -1
    &
    (for i be Nat st 1<=i & i <=k+1 holds
    m.(i+1) = m.i * b.i );

    P14: k <= k +1 by NAT_1:12;

    per cases;
    suppose P15: k = 0;

      P16: m.((k+1)+1)
      = m.1 * b.1 by P12,P15
      .= b.1 by A2;

      for j be Nat st (k+1)+1 <= j & j <= len b
      holds
      m.((k+1)+1),b.j are_relative_prime
      proof
        let j be Nat;
        assume XX0:(k+1)+1 <= j & j <= len b;
        then
        XX2: 1 <= j & j <= len b by XXREAL_0:2,P15;
        then
        XX1: j in Seg(len b) by FINSEQ_1:1;
        1 <= 1 & 1 <= len b by XXREAL_0:2,XX2;
        then
        XX3: 1 in Seg(len b);

        1 <> j by XX0,P15;
        hence
        m.((k+1)+1),b.j are_relative_prime by P16,A2,XX1,XX3;
      end;
      hence thesis;
    end;
    suppose P19:k <> 0;

      P20: now let i be Nat;
      assume 1<=i & i <=k;
      then
      1<=i & i <=(k +1) by NAT_1:12;

      hence m.(i+1) = m.i * b.i by P12;
    end;

    thus
    for j be Nat st (k+1)+1 <= j & j <= len b
    holds

    m.((k+1)+1),b.j are_relative_prime
    proof
      let j be Nat;

      assume XX6:(k+1) +1 <= j & j <= len b;
      (k +1) <= (k+1) +1 by NAT_1:12;
      then

      XX1: k +1 <= j & j <= len b by XX6,XXREAL_0:2;
      then
      P21: m.(k+1),b.j are_relative_prime
      by P20,P11,P12,P14,XXREAL_0:2,NAT_1:14,P19;

      XX2: 1<= k+1 by NAT_1:12;
      k +1 <= len b by XX1,XXREAL_0:2;
      then
      XX3: k+1 in Seg (len b) by XX2;
      1<=j & j <= len b by XX1,XX2,XXREAL_0:2;
      then
      XX4: j in Seg (len b) by FINSEQ_1:1;

      (k+1) < j by XX6,XXREAL_0:2,NAT_1:16;
      then
      P23:
      b.(k+1),b.j are_relative_prime by A2,XX3,XX4;
      m.((k+1)+1) = m.(k+1) * b.(k+1) by P12;
      hence
      m.((k+1)+1),b.j are_relative_prime by P23,P21,INT_2:26;
    end;
  end;
end;
for k be Element of NAT holds P[k] from NAT_1:sch 1(P0,P1);
hence thesis;
end;

LmTh6:
for b,m be FinSequence of INT
st len b = len m
&
m.1 = 1
holds
for k be Element of NAT
st
1<= k & k <= len b -1
&
(for i be Nat st 1<=i & i <=k
holds
m.(i+1) = m.i * b.i )
holds
for j be Nat st 1<= j & j <=k
holds
m.(k+1) mod b.j = 0
proof
  let b,m be FinSequence of INT;
  assume len b = len m;
  assume A2: m.1 = 1;
  defpred P[Nat] means
  ( 1<= $1 & $1 <= len b -1
  &
  (for i be Nat st
  1<=i & i <=$1
  holds
  m.(i+1) = m.i * b.i ) )
  implies
  for j be Nat st 1<=j & j <=$1
  holds
  m.($1+1) mod b.j = 0;
  reconsider I0=0 as Element of NAT;
  P0:P[0];

  P1:for k be Element of NAT st P[k] holds P[k+1]
  proof
    let k be Element of NAT;
    assume P11: P[k];
    assume P12:

    1<= k+1 & k+1 <= len b -1

    &
    (for i be Nat st

    1<=i & i <=k+1
    holds
    m.(i+1) = m.i * b.i );
    P14: k <= k +1 by NAT_1:12;

    per cases;
    suppose P15: k = 0;
      P16: m.((k+1)+1)
      = m.1 * b.1 by P12,P15
      .= b.1 by A2;

      for j be Nat st 1<= j & j <= (k+1)
      holds
      m.((k+1)+1) mod b.j =0
      proof
        let j be Nat;
        assume 1<= j & j <=(k+1);
        then
        j = 1 by XXREAL_0:1,P15;
        hence
        m.((k+1)+1) mod b.j = 0 by INT_1:50,P16;
      end;
      hence thesis;
    end;
    suppose k <> 0;
      P20: now let i be Nat;
      assume 1<=i & i <=k;
      then
      1<=i & i <=(k +1) by NAT_1:12;
      hence m.(i+1) = m.i * b.i by P12;
    end;
    thus for j be Nat st 1 <=j & j <= k+1 holds m.((k+1)+1) mod b.j = 0
    proof
      let j be Nat;
      assume XX6:1 <=j & j <= k+1;
      reconsider bj =b.j as Element of INT by INT_1: def 2;
      per cases;
      suppose XX61: j = k+1;
        thus m.((k+1)+1) mod b.j
        = (m.(k+1) * b.(k+1)) mod b.j by P12
        .= ((m.(k+1) mod b.j ) *( b.(k+1) mod b.j ) )
        mod b.j by NAT_D:67
        .= ((m.(k+1) mod b.j ) * (0 qua Nat) )
        mod b.j by INT_1:50,XX61
        .= 0 by INT_4:12;
      end;
      suppose j <> k+1;
        then
        j < k+1 by XX6,XXREAL_0:1;
        then
        XX1: j <= k by NAT_1:13;
        thus m.((k+1)+1) mod b.j
        = (m.(k+1) * b.(k+1)) mod b.j by P12
        .= ((m.(k+1) mod b.j ) *( b.(k+1) mod b.j ) )
        mod b.j by NAT_D:67
        .= ( 0 *( b.(k+1) mod b.j ) )
        mod b.j by XX1,P20,XX6,P11,P12,P14,XXREAL_0:2
        .= 0 by INT_4:12;
      end;
    end;
  end;
end;
for k be Element of NAT holds P[k] from NAT_1:sch 1(P0,P1);
hence thesis;
end;

theorem Th4:
  for nlist be non empty FinSequence of [:INT,INT:],
  a,b be FinSequence of INT
  st len a = len b & len a = len nlist
  &
  (for i be Nat st i in Seg (len nlist)
  holds b.i <> 0 )
  &
  (for i be Nat st i in Seg (len nlist)
  holds
  (nlist.i)`1 = a.i & (nlist.i)`2 = b.i )
  &
  (for i,j be Nat st i in Seg (len nlist)
  & j in Seg (len nlist)
  & i <> j
  holds b.i,b.j are_relative_prime )
  holds
  for i be Nat st i in Seg (len nlist)
  holds ALGO_CRT(nlist) mod b.i = a.i mod b.i
  proof
    defpred P[Nat] means
    for nlist be non empty FinSequence of [:INT,INT:],
    a,b be FinSequence of INT
    st len nlist = $1
    & len a = len b
    & len a = len nlist
    & (for i be Nat st i in Seg (len nlist)
    holds b.i <> 0 )
    &
    (for i be Nat st i in Seg (len nlist)
    holds
    (nlist.i)`1 = a.i & (nlist.i)`2 = b.i )
    &
    (for i,j be Nat st i in Seg (len nlist)
    & j in Seg (len nlist)
    & i <> j
    holds b.i,b.j are_relative_prime)
    holds
    (for i be Nat st i in Seg (len nlist)
    holds ALGO_CRT(nlist) mod b.i = a.i mod b.i
    );

    P0: P[ 0 ];

    P1: for n be Element of NAT st P[ n ] holds P[n+1]
    proof
      let n be Element of NAT;

      assume AS1:P[n];
      let nlist be non empty FinSequence of [:INT,INT:],
      a,b be FinSequence of INT;
      assume AS2: len nlist = n+1
      & len a = len b
      & len a = len nlist
      & (for i be Nat st i in Seg (len nlist)
      holds b.i <> 0 )
      &
      (for i be Nat st i in Seg (len nlist)
      holds
      (nlist.i)`1 = a.i & (nlist.i)`2 = b.i )
      &
      (for i,j be Nat st i in Seg (len nlist)
      & j in Seg (len nlist)
      & i <> j
      holds b.i,b.j are_relative_prime );

      per cases;
      suppose P1: n = 0;
        P2: 1 in Seg(len nlist) by P1,AS2;
        P3: ALGO_CRT(nlist) = (nlist.1)`1 by defALGOCRT,P1,AS2
        .= a.1 by AS2,P2;
        thus
        for i be Nat st i in Seg (len nlist)
        holds ALGO_CRT(nlist) mod b.i = a.i mod b.i
        by P3,TARSKI:def 1,FINSEQ_1:2,P1,AS2;
      end;
      suppose NN1: n <> 0;
        then
        NN2: 1 <=n by NAT_1:14;

        P4: len nlist <> 1 by AS2,NN1;

        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;

        KK: n <= n+1 by NAT_1:11;
        then
        D02: len a1 = n by FINSEQ_1:59,AS2;

        D22: len nlist1 = n by KK,FINSEQ_1:59,AS2;
        then
        reconsider nlist1 as non empty FinSequence of [:INT,INT:]
        by NN1;

        D23: dom nlist1 = Seg (len nlist1) by FINSEQ_1:def 3
        .= Seg n by KK,FINSEQ_1:59,AS2;
        D25: len nlist1 = n by D23,FINSEQ_1:def 3;
        then
        D28: Seg len nlist1 c= Seg (len nlist) by KK,FINSEQ_1:5,AS2;

        X1: len nlist1 = n
        & len a1 = len b1
        & len a1 = len nlist1 by D02,KK,FINSEQ_1:59,AS2;

        X2A:for i be Nat st i in Seg (len nlist1)
        holds b1.i <> 0
        proof
          let i be Nat;
          assume D260: i in Seg (len nlist1);
          then
          b1.i =b.i by FUNCT_1:49,D25;
          hence thesis by D28,D260,AS2;
        end;

        X2:for i be Nat st i in Seg (len nlist1)
        holds
        (nlist1.i)`1 = a1.i & (nlist1.i)`2 =b1.i
        proof
          let i be Nat;
          assume X21: i in Seg (len nlist1);

          X23:(nlist1.i)`1 = (nlist.i)`1 by X21,FUNCT_1:49,D25
          .= a.i by X21,D28,AS2
          .= a1.i by X21,FUNCT_1:49,D25;
          (nlist1.i)`2 = (nlist.i)`2 by X21,FUNCT_1:49,D25
          .= b.i by X21,D28,AS2
          .= b1.i by X21,FUNCT_1:49,D25;
          hence thesis by X23;
        end;

        X3:
        for i,j be Nat st i in Seg (len nlist1)
        & j in Seg (len nlist1)
        & i<>j
        holds b1.i,b1.j are_relative_prime
        proof
          let i,j be Nat;
          assume A1: i in Seg (len nlist1)
          & j in Seg (len nlist1)
          & i <> j;

          A3: b.i = b1.i by A1,FUNCT_1:49,D25;
          b.j = b1.j by A1,FUNCT_1:49,D25;
          hence thesis by A3,A1,D28,AS2;
        end;

        X400:for i be Nat st i in Seg (len nlist1)
        holds ALGO_CRT(nlist1) mod b.i = a.i mod b.i
        proof
          let i be Nat;
          assume A1: i in Seg (len nlist1);
          then
          a1.i = a.i & b1.i =b.i by FUNCT_1:49,D25;
          hence
          ALGO_CRT(nlist1) mod b.i = a.i mod b.i by AS1,X1,X2,X3,X2A,A1;
        end;

        consider
        m,l,prodc,prodi be FinSequence of INT,
        M0,M be Element of INT such that
        X5:
        len m = len nlist
        & len l = len nlist
        & len prodc = len nlist - 1
        & len prodi = len nlist - 1
        & m.1 =1
        & (for i be Nat
        st 1<=i & i<=(len m) - 1
        holds
        ex d,x,y be 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 be Nat
        st 1<=i & i<=len m - 1
        holds
        ex u,u0,u1 be 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 P4,defALGOCRT;

        LmTh51: 1 + 1 <= n + 1 by XREAL_1:6,NN2;

        reconsider lb1=len b -1 as Element of NAT by AS2;

        LmTh54:1<= lb1 & lb1 <= lb1 by AS2,NAT_1:14,NN1;
        LmTh55:
        for i be Nat st 1<=i & i <=lb1
        holds
        m.(i+1) = m.i * b.i

        proof
          let i be Nat;
          assume PX0: 1<=i & i <=lb1;
          then
          PX1: ex d,x,y be 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 AS2,X5;
          i in Seg (len nlist1) by PX0,D22,AS2,FINSEQ_1:1;
          hence
          m.(i+1) = m.i * b.i by PX1,AS2,D28;
        end;

        LmTh56:m.(len nlist ),b.(len nlist) are_relative_prime
        by AS2,LmTh5,LmTh51,X5,LmTh54,LmTh55;

        set l1 = l | n, m1 = m | n;

        KK: n <= n+1 by NAT_1:11;
        then
        PD02: len l1 = n by AS2,FINSEQ_1:59,X5;

        PD11: dom m1 = Seg (len m1) by FINSEQ_1:def 3
        .= Seg n by AS2,FINSEQ_1:59,X5,KK;
        PD12: len m1 = n by PD11,FINSEQ_1:def 3;
        1 -1 <=n - 1 by NN2,XREAL_1:9;
        then
        n -1 in NAT by INT_1:3;
        then
        reconsider nn1 = n-1 as Nat;
        reconsider prodi1 = prodi | nn1 as FinSequence of INT;
        reconsider prodc1 = prodc | nn1 as FinSequence of INT;

        XX5: n - 1 <= n - 0 by XREAL_1:10;
        then
        QD02: len prodi1 = nn1 by AS2,X5,FINSEQ_1:59;
        QD12: len prodc1 = nn1 by XX5,AS2,X5,FINSEQ_1:59;

        PD24: 1 in Seg n by NN2;

        PD26X: l1.1 = l.1 by FUNCT_1:49,PD24
        .= (nlist1.1)`1 by FUNCT_1:49,PD24,X5;

        QKK: n - 1 <= n - 0 by XREAL_1:10;

        PD26: now let i be Nat;
        assume PD260X: 1<=i & i<=len m1 - 1;
        then
        PD260: 1<=i & i<=len m1 by PD12,QKK,XXREAL_0:2;
        then
        i in Seg (len m1) by FINSEQ_1:1;
        hence
        m1.i =m.i by FUNCT_1:49,PD12;

        i in Seg (len l1) by FINSEQ_1:1,PD260,PD02,PD12;
        hence
        l1.i =l.i by FUNCT_1:49,PD02;

        i in Seg (len prodi1) by FINSEQ_1:1,PD260X,PD12,QD02;
        hence
        prodi1.i =prodi.i by FUNCT_1:49,QD02;

        i in Seg (len prodc1) by FINSEQ_1:1,PD260X,PD12,QD12;
        hence
        prodc1.i =prodc.i by FUNCT_1:49,QD12;
      end;

      (len m1) in Seg (len nlist1) by D22,PD12,FINSEQ_1:3;
      then
      Z1: (len m1) in Seg (len nlist) by D28;

      Z2: nlist1.(len m1) = nlist.(len m1) by FUNCT_1:49,D22,PD12,FINSEQ_1:3;

      (len m1) in dom nlist by FINSEQ_1:def 3,Z1;
      then
      nlist1.(len m1) in [:INT,INT:] by FINSEQ_2:11,Z2;
      then
      reconsider M01 = (nlist1.(len m1))`2 as Element of INT by MCART_1:10;

      reconsider M1 = (prodc1.((len m1)-1))*M01
      as Element of INT by INT_1:def 2;
      QX1: len m1 = len nlist1
      & len l1 = len nlist1
      & len prodc1 = len nlist1 - 1
      & len prodi1 = len nlist1 - 1
      & m1.1 =1 by KK,FINSEQ_1:59,AS2,PD12,PD02,QD12,QD02,X5,FUNCT_1:49,PD24;
      QX2: for i be Nat
      st 1<=i & i<=(len m1) - 1
      holds
      ex d,x,y be Element of INT
      st x = (nlist1.i)`2
      &
      m1.(i+1) = m1.i * x
      &
      y = m1.(i+1)
      &
      d = (nlist1.(i+1))`2
      &
      prodi1.i = ALGO_INVERSE(y,d)
      &
      prodc1.i = y
      proof
        let i be Nat;
        assume XQ21: 1<=i & i<=(len m1) - 1;
        then
        XQ22:m1.i = m.i by PD26;
        XQ23:prodi1.i = prodi.i by PD26,XQ21;
        XQ24:prodc1.i = prodc.i by PD26,XQ21;

        XQ25: 1<=i+1 by NAT_1:12;
        i+1 <=(len m1) - 1 +1 by XQ21,XREAL_1:6;
        then
        YY1: i+1 in Seg (len m1) by XQ25;
        then
        XQ27:m1.(i+1) =m.(i+1) by FUNCT_1:49,PD12;

        XQ28: 1<=i & i<=len m1 by XQ21,PD12,QKK,XXREAL_0:2;

        XQ30: 1<=i & i <= len m - 1 by X5,AS2,XQ21,PD12,QKK,XXREAL_0:2;

        i in Seg (len nlist1) by PD12,D22,XQ28,FINSEQ_1:1;
        then
        XQ32: nlist1.i = nlist.i by FUNCT_1:49,D25;

        nlist1.(i+1) = nlist.(i+1) by FUNCT_1:49,PD12,YY1;
        hence thesis by XQ22,XQ23,XQ24,XQ27,XQ30,XQ32,X5;
      end;

      QX4: for i be Nat
      st 1<=i & i<=len m1 - 1
      holds
      ex u,u0,u1 be Element of INT
      st
      u0 = ( nlist1.(i+1))`1
      &
      u1 = ( nlist1.(i+1))`2
      &
      u = ( (u0- l1.i)*(prodi1.i)) mod u1
      & l1.(i+1) = l1.i + u*(prodc1.i)
      proof
        let i be Nat;
        assume XQ21: 1<=i & i<=(len m1) - 1;
        then
        XQ22:l1.i = l.i by PD26;
        XQ23:prodi1.i = prodi.i by PD26,XQ21;
        XQ24:prodc1.i = prodc.i by PD26,XQ21;
        XQ25: 1<=i+1 by NAT_1:12;
        i+1 <=(len m1) - 1 +1 by XQ21,XREAL_1:6;
        then
        YY1: i+1 in Seg (len m1) by XQ25;
        then
        XQ27:l1.(i+1) =l.(i+1) by FUNCT_1:49,PD12;
        XQ30: 1<=i & i <= len m - 1 by X5,AS2,XQ21,PD12,QKK,XXREAL_0:2;
        nlist1.(i+1) = nlist.(i+1) by FUNCT_1:49,PD12,YY1;
        hence thesis by XQ22,XQ23,XQ24,XQ27,XQ30,X5;
      end;

      reconsider s= l1.(len m1) mod M1 as Element of INT by INT_1:def 2;

      QX12: 1 <= (len m) - 1 by X5,AS2,NAT_1:14,NN1;
      reconsider lm1= (len m) - 1 as Element of NAT by X5;

      QX13: 1<=lm1 & lm1 <= (len m) - 1 by X5,AS2,NAT_1:14,NN1;

      consider d,x,y be Element of INT such that
      QX14: 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 X5,AS2,NN2;

      consider u,u0,u1 be Element of INT such that
      QX15:
      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 QX13,X5;

      QX43: len nlist in Seg (len nlist) by FINSEQ_1:3;
      QX45: M0 = b.(len nlist) by X5,AS2,QX43;
      then
      QX37B: M0 <> 0 by QX43,AS2;
      QX36A:
      (u0-l.(len m -1) )* ALGO_INVERSE(y,M0) is Element of INT
      by INT_1:def 2;
      consider r be Element of INT such that
      QX37:u = (u0-l.(len m -1) )* ALGO_INVERSE(y,M0)
      + r*M0 by LmTh4,X5,QX14,QX15,QX36A,QX37B;

      QX26A: y <> 0 by QX14,X5,AS2,LmTh5A,LmTh54,LmTh55;

      now per cases;
        suppose AA1:len nlist1 = 1;

          AAA1: ALGO_CRT(nlist1) = (nlist1.1)`1 by AA1,defALGOCRT
          .= (nlist.1)`1 by FUNCT_1:49,PD24
          .= l.(len m-1) by AA1,AS2,X5,D23,FINSEQ_1:def 3;
          QX27: ALGO_CRT(nlist)
          =(l.(len m -1) + u*y ) mod M by QX14,QX15,X5;

          reconsider p=0 as Element of INT by INT_1:def 2;
          QX28:ALGO_CRT(nlist1) = l.(len m-1) + p * y by AAA1;

          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;
          M = y*M0 by X5,QX14;
          then consider t be Element of INT such that
          QX30:ALGO_CRT(nlist) =ly + t* M
          by LmTh4,QX27,QX37B,QX26A,XCMPLX_1:6;

          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 X5,QX14,QX37,QX30,AAA1;
          hence
          ex p,qr be 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 QX28;
        end;

        suppose AA2:len nlist1 <> 1;
          then
          QX7: ALGO_CRT(nlist1) = s by defALGOCRT,QX1,QX2,QX4,PD26X
          .= l1.(len m1) mod ((prodc1.((len m1)-1))*M01);

          QX8: l1.(len l1) =l.(len l1)
          by FUNCT_1:49,NN1,PD02,FINSEQ_1:3
          .=l.(len m -1) by X5,AS2,FINSEQ_1:59,KK;

          2 <= len nlist1 by AA2,NAT_1:23;
          then
          2 - 1 <= len m1 - 1 by XREAL_1:9,PD12,X1;
          then
          QX90: 1 <= nn1 & nn1 <= len m1 - 1 by PD11,FINSEQ_1:def 3;

          QX10:M01 = (nlist.(len m1))`2 by FUNCT_1:49,D22,PD12,FINSEQ_1:3
          .= (nlist.(len m -1 ))`2 by X5,AS2,PD11,FINSEQ_1:def 3;

          consider d1,x1,y1 be Element of INT such that
          QX16: x1 = (nlist1.nn1)`2 &
          m1.(nn1+1) = m1.nn1 * x1 &
          y1 = m1.(nn1+1) &
          d1 = (nlist1.(nn1+1))`2 &
          prodi1.nn1 = ALGO_INVERSE(y1,d1) &
          prodc1.nn1 = y1 by QX2,QX90;

          QX21:len m1
          = len m-1 by X5,AS2,PD11,FINSEQ_1:def 3;
          then
          QX20:lm1 in Seg (len m1) by QX12;

          QX24:ALGO_CRT(nlist1)
          =l.(len m-1) mod (y1*M01)
          by QX16,QX7,QX21,QX8,AS2,FINSEQ_1:59,X5,KK;
          QX24A:
          ALGO_CRT(nlist1) is Element of INT
          &
          l.(len m-1) is Element of INT
          &
          (y1*M01) is Element of INT by INT_1:def 2;

          QX26:y =y1 * x by QX16,X5,AS2,FUNCT_1:49,PD12,QX20,QX14;
          then
          QX26C: y1*M01 <> 0 by X5,AS2,LmTh5A,LmTh54,LmTh55,QX10,QX14;
          consider p be Element of INT such that
          QX30:ALGO_CRT(nlist1) = l.(len m-1) + p* (y1*M01)
          by QX24,LmTh4,QX24A,QX26A,QX10,QX14,QX26;

          QX27: ALGO_CRT(nlist)
          = (l.(len m -1) + u*(y1*x) ) mod ((prodc.((len m)-1))*M0)
          by QX16,X5,AS2,FUNCT_1:49,PD12,QX20,QX14,QX15
          .= (l.(len m -1) + u*(y1*x) )
          mod (y1*x*M0) by QX16,X5,AS2,FUNCT_1:49,PD12,QX20,QX14;

          ALGO_CRT(nlist) is Element of INT
          &
          l.(len m -1) + u*(y1*x) is Element of INT
          &
          (y1*x*M0) is Element of INT by INT_1:def 2;
          then
          consider q be Element of INT such that
          QX31:ALGO_CRT(nlist) = l.(len m -1) + u*(y1*x)
          + q* (y1*x*M0) by QX27,LmTh4,QX10,QX14,QX26C,XCMPLX_1:6,QX37B;

          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 QX10,QX14
          .= ALGO_CRT(nlist1) -((l.(len m -1) )*ALGO_INVERSE(y,M0)*y + p*y )
          + r*M0*y + u0* ALGO_INVERSE(y,M0)*y
          by QX26,QX37;
          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 QX16,X5,AS2,FUNCT_1:49,PD12,QX20,QX14,QX31,QX30
          .= 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 be 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 QX30,QX26,QX10,QX14;
        end;
      end;

      then consider p,qr be Element of INT such that
      QX41:
      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,M0 are_relative_prime by QX37B,LmTh4A,QX14,X5,QX45,LmTh56;
      then
      y0 gcd M0 = 1 by INT_2:def 3;
      then
      QX48: ALGO_EXGCD(M0,y0)`3_3 = 1 by Th2;

      QX50:
      ((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 QX48,Th3
      .= (l.(len m -1) * 1 ) mod M0
      + (p*y mod M0) mod M0
      by NAT_D:67
      .= ALGO_CRT(nlist1) mod M0 by QX41,NAT_D:66;
      thus
      for i be Nat st i in Seg (len nlist)
      holds ALGO_CRT(nlist) mod b.i = a.i mod b.i

      proof
        let i be Nat;
        assume VA0: i in Seg (len nlist);
        then
        VA1:1 <= i & i <= len nlist by FINSEQ_1:1;

        per cases;
        suppose VA2: i = len nlist;
          VA22: b.i <> 0 by AS2,VA0;

          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;
          VA31:
          K2y mod b.i = (((qr)*y) mod M0) *( M0 mod M0) mod M0
          by QX45,VA2,NAT_D:67
          .= ( (( (qr)*y ) mod M0 ) *I0 ) mod M0 by INT_1:50
          .= I0 mod b.i by VA2,X5,AS2,QX43;

          VA30:
          K4y mod b.i
          = ((I0 mod b.i) + (K3y mod b.i)) mod b.i by VA31,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 QX48,Th3,VA2,QX45
          .= (u0 * 1 ) mod b.i by NAT_D:67
          .= a.i mod b.i by VA2,QX43,X5,AS2,QX15;

          VA31:
          (ALGO_CRT(nlist) + (K1y) ) mod b.i
          = ((ALGO_CRT(nlist) mod b.i) + (ALGO_CRT(nlist1) mod b.i) )
          mod b.i by QX50,VA2,QX45,NAT_D:66
          .= (ALGO_CRT(nlist) + ALGO_CRT(nlist1) ) mod b.i by NAT_D:66;
          VA32:
          (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 NAT_D:66,VA30;
          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 be Element of INT such that
          VA33: LL = LL1 + r *bi
          by LmTh4,VA22,VA31,VA32,QX41;

          reconsider LL2= ALGO_CRT(nlist1) + a.i
          as Element of INT by INT_1:def 2;

          consider s be Element of INT such that
          VA34: LL = LL2 + s *bi by LmTh4,VA22;
          reconsider LL3= s -r as Element of INT by INT_1:def 2;
          VA36:
          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 VA33,VA34
          .= ((a.i mod b.i ) + (I0 mod b.i) ) mod b.i
          by VA36,NAT_D:66
          .= ( a.i + I0 ) mod b.i by NAT_D:66
          .= a.i mod b.i;
        end;
        suppose i <> len nlist;
          then
          i < len nlist by VA1,XXREAL_0:1;
          then
          i + 1 <= len nlist by NAT_1:13;
          then
          VA22P:i + 1 - 1 <= len nlist -1 by XREAL_1:9;
          then
          VA22: 1<= i & i <= len nlist1 by KK,FINSEQ_1:59,AS2,FINSEQ_1:1,VA0;
          VA24:i in Seg (len nlist1) by FINSEQ_1:1,VA22P,AS2,X1,VA1;

          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;
          VA27: y mod b.i = 0 by X1,QX14,LmTh6,LmTh54,LmTh55,AS2,X5,VA22;

          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;
          VA29:
          (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 VA27;
          VA30:
          (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 VA27;
          VA31:
          (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 NAT_D:66,VA29
          .=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 NAT_D:66,VA30
          .=ALGO_CRT(nlist1) mod b.i;
          hence
          ALGO_CRT(nlist) mod b.i = a.i mod b.i by VA24,QX41,VA31,X400;
        end;
      end;
    end;
  end;
  for n be Element of NAT holds P[n] from NAT_1:sch 1(P0,P1);
  hence thesis;
end;

LmTh7A:
for x,y,a,b be Element of INT
st x mod a = y mod a
& x mod b = y mod b
& a,b are_relative_prime
holds
x mod (a*b) = y mod (a*b)
proof
  let x,y,a,b be Element of INT;
  assume
  AS: x mod a = y mod a
  & x mod b = y mod b
  & a,b are_relative_prime;

  set g1 = x mod a;
  set g2 = x mod b;

  per cases;
  suppose C1: a*b = 0;
    thus
    x mod (a*b)
    =0 by INT_1:def 10,C1
    .= y mod (a*b) by C1,INT_1:def 10;
  end;
  suppose a*b <> 0;
    then
    C3: a <> 0 & b <> 0;

    C5: y = (y div a)*a + (y mod a) by C3,INT_1:59;
    C6: x = (x div b)*b + (x mod b) by C3,INT_1:59;

    x-y = (x div a)*a + (x mod a)
    - ((y div a)*a + (y mod a)) by C3,INT_1:59,C5
    .= ((x div a) - (y div a)) *a by AS;
    then
    a divides x-y by INT_1:def 3;
    then
    C8: x,y are_congruent_mod a by INT_1:def 4;
    x-y = (x div b)*b + (x mod b)
    - ((y div b)*b + (y mod b)) by C3,INT_1:59,C6
    .= ((x div b) - (y div b)) *b by AS;
    then
    b divides x-y by INT_1:def 3;
    then
    x,y are_congruent_mod b by INT_1:def 4;
    then
    x,y are_congruent_mod (a*b)
    by AS,C8,INT_6:21;
    then
    (a*b) divides x-y by INT_1:def 4;
    then
    consider p be Integer
    such that C11: x-y = (a*b)*p by INT_1:def 3;

    reconsider I0 =0 as Element of INT by INT_1:def 2;

    thus
    x mod (a*b) = (y + (a*b)*p ) mod (a*b) by C11
    .= ( (y mod (a*b)) + ( ((a*b)*p) mod (a*b) ) ) mod (a*b)
    by NAT_D:66
    .= ((y mod (a*b))
    + (( ((a*b) mod (a*b)) * (p mod (a*b)) ) mod (a*b) ))
    mod (a*b) by NAT_D:67
    .= ((y mod (a*b)) + (( I0* (p mod (a*b)) ) mod (a*b)) )
    mod (a*b) by INT_1:50
    .= ((y + I0)) mod (a*b) by NAT_D:66
    .= y mod (a*b);
  end;
end;

theorem LmTh7:
  for x,y be Element of INT,
  b,m be non empty FinSequence of INT
  st
  2 <=len b
  &
  (for i,j be Nat st i in Seg (len b)
  & j in Seg (len b)
  & i <> j
  holds b.i,b.j are_relative_prime )
  &
  (for i be Nat
  st i in Seg len b
  holds x mod b.i = y mod b.i )
  &
  m.1 = 1 holds
  for k be Element of NAT
  st
  1<= k & k <= len b
  &
  (for i be Nat st 1<=i & i <=k
  holds
  m.(i+1) = m.i * b.i )
  holds
  x mod m.(k+1) = y mod m.(k+1)
  proof
    let x,y be Element of INT,
    b,m be non empty FinSequence of INT;
    assume
    A1: 2 <=len b;
    assume
    A4:
    for i,j be Nat st i in Seg (len b)
    & j in Seg (len b)
    & i <> j
    holds b.i,b.j are_relative_prime;
    assume
    A2:
    for i be Nat
    st i in Seg len b
    holds x mod b.i = y mod b.i;
    assume
    A3:
    m.1 = 1;

    defpred P[Nat] means
    ( 1<= $1 & $1 <= len b
    &
    (for i be Nat st 1<=i & i <=$1
    holds
    m.(i+1) = m.i * b.i ) )
    implies
    x mod m.($1+1) = y mod m.($1+1);

    reconsider I0=0 as Element of NAT;
    P0:P[0];

    P1:for k be Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT;
      assume P11: P[k];
      assume P12:
      1<= k+1 & k+1 <= len b
      &
      (for i be Nat st
      1<=i & i <=k+1
      holds
      m.(i+1) = m.i * b.i );

      P14: k <= k +1 by NAT_1:12;

      per cases;
      suppose P15: k = 0;
        P16: m.((k+1)+1)
        = m.1 * b.1 by P12,P15
        .= b.1 by A3;

        1<= 1 & 1<= len b by NAT_1:14;
        then
        P18: 1 in Seg len b;
        thus
        x mod m.((k+1)+1)
        = y mod m.((k+1)+1) by P16,P18,A2;
      end;
      suppose P181:k <> 0;

        k+1 -1 <= len b -1 by P12,XREAL_1:9;
        then
        P19: 1<=k & k <= len b -1 by P181,NAT_1:14;

        XX1: now let i be Nat;
        assume 1<=i & i <=k;
        then

        1<=i & i <=(k +1) by NAT_1:12;

        hence
        m.(i+1) = m.i * b.i by P12;
      end;
      P22: m.((k+1)+1) = m.(k+1) * b.(k+1) by P12;
      k+1 in Seg len b by P12;
      then
      P23: x mod b.(k+1) = y mod b.(k+1) by A2;
      P24: m.(k+1),b.(k+1) are_relative_prime
      by LmTh5,XX1,P19,A1,A4,A3,P12;
      m.(k+1) is Element of INT & b.(k+1) is Element of INT
      by INT_1:def 2;
      hence
      x mod m.((k+1)+1) = y mod m.((k+1)+1)
      by P22,P23,P11,NAT_1:14,P181,P12,P14,XXREAL_0:2,XX1,P24,LmTh7A;
    end;

  end;
  for k be Element of NAT holds P[k] from NAT_1:sch 1(P0,P1);
  hence thesis;
end;

theorem LmTh8:
  for b be FinSequence of INT
  st len b = 1 holds Product b = b.1
  proof
    let b be FinSequence of INT;
    assume len b = 1;
    then
    b = <*b.1*> by FINSEQ_1:40;
    hence Product b = b.1 by RVSUM_1:95;
  end;

theorem LmTh9:
  for b be FinSequence of INT
  ex m be non empty FinSequence of INT
  st
  len m = len b + 1
  &
  m.1 = 1
  &
  (for i be Nat st 1<=i & i <=len b
  holds
  m.(i+1) = m.i * b.i )
  &
  Product b = m.(len b + 1 )
  proof
    defpred P[Nat]
    means
    for b be FinSequence of INT
    st
    len b = $1
    holds
    ex m be non empty FinSequence of INT
    st
    ( len m = len b + 1
    &
    m.1 = 1
    &
    (for i be Nat st 1<=i & i <=len b
    holds
    m.(i+1) = m.i * b.i ) )
    & Product b = m.(len b + 1);

    P0: P[0]
    proof
      let b be FinSequence of INT;
      assume A1:len b = 0;

      I0: 1 in INT by INT_1:def 2;
      rng (<*(1 qua Integer ) *>) = {(1 qua Integer)} by
      FINSEQ_1:39;
      then
      rng (<*(1 qua Integer ) *>) c= INT
      by ZFMISC_1:31,I0;
      then
      reconsider m=<*(1 qua Integer ) *>
      as non empty FinSequence of INT by FINSEQ_1:def 4;
      P0: len m = len b + 1 by A1,FINSEQ_1:40;
      P1: m.1 = 1 by FINSEQ_1:40;
      P2: for i be Nat st 1<=i & i <=len b
      holds
      m.(i+1) = m.i * b.i by A1;

      b = <*>REAL by A1;
      hence thesis by P0,P1,P2,A1,RVSUM_1:94;
    end;
    P1: for k be Element of NAT st P[k] holds P[k+1]
    proof
      let k be Element of NAT;
      assume A1: P[k];

      let b be FinSequence of INT;
      assume A2: len b = k+1;
      set b1 = b | k;

      P2: len b1 = k by FINSEQ_1:59,A2,NAT_1:12;

      then
      consider m1 be non empty FinSequence of INT such that
      P4:
      (
      len b1 + 1 = len m1
      &
      m1.1 = 1
      &
      (for i be Nat st 1<=i & i <=len b1
      holds
      m1.(i+1) = m1.i * b1.i ) )
      & Product b1 = m1.(len b1+1) by A1;

      set m = m1 ^ <* (Product b1)*b.(len b) *>;

      P5Z: (Product b1)*b.(len b) in INT by P4,INT_1:def 2;
      P5W: rng (<*(Product b1)*b.(len b) *>)
      = {(Product b1)*b.(len b)} by FINSEQ_1:39;
      then
      P5Q: rng (<* (Product b1)*b.(len b) *>) c= INT
      by ZFMISC_1:31,P5Z;

      P5: len m = len m1 + len (<* (Product b1)*b.(len b) *>)
      by FINSEQ_1:22
      .= (len b1 + 1) + 1 by P4,FINSEQ_1:40
      .= len b + 1 by FINSEQ_1:59,A2,NAT_1:12;

      VV2: rng m = rng m1 \/ {(Product b1)*b.(len b)}
      by FINSEQ_1:31,P5W;
      rng m1 c= INT by FINSEQ_1:def 4;
      then
      rng m c= INT by P5W,VV2,P5Q,XBOOLE_1:8;

      then
      reconsider m as non empty FinSequence of INT by FINSEQ_1:def 4;


      P5B: len m1 = len b1 + 1 by P4
      .= k + 1 by FINSEQ_1:59,A2,NAT_1:12;

      1 <= 1 & 1 <=k+1 by NAT_1:12;
      then
      1 in Seg (len m1) by P5B;
      then
      1 in dom m1 by FINSEQ_1:def 3;
      then

      P8: m.1 =1 by P4,FINSEQ_1:def 7;

      P9:for i be Nat st 1<=i & i <=len b
      holds
      m.(i+1) = m.i * b.i
      proof
        let i be Nat;
        assume P10: 1<=i & i <=len b;
        per cases;
        suppose P11: i = len b;

          len b1+1 in Seg (len m1) by P2,P5B,FINSEQ_1:4;
          then
          len b1+1 in dom m1 by FINSEQ_1:def 3;
          then

          P13: m1.(len b1+1) = m.(len b1+1) by FINSEQ_1:def 7
          .= m.i by A2,FINSEQ_1:59,NAT_1:12,P11;

          1 in Seg 1;
          then
          P13C: 1 in dom (<* (Product b1)*b.(len b) *>)
          by FINSEQ_1:38;
          thus m.(i+1) = (<* (Product b1)*b.(len b) *>).1
          by FINSEQ_1:def 7,P11,A2,P5B,P13C
          .= m.i * b.i by P13,P11,P4,FINSEQ_1:40;
        end;
        suppose i <> len b;
          then
          P12D: i < len b by P10,XXREAL_0:1;
          then
          P12A: 1<=i & i <=len b1 by P2,A2,NAT_1:13,P10;
          then P13: m1.(i+1) = m1.i * b1.i by P4;
          i in Seg(len m1) by FINSEQ_1:1,P10,A2,P5B;
          then
          P13B: i in dom m1 by FINSEQ_1:def 3;
          P13E:i +1 <= len m1 by A2,P5B,P12D,NAT_1:13;
          1 <= i + 1 by NAT_1:12;
          then
          i+1 in Seg(len m1) by P13E;
          then
          P13C: i+1 in dom m1 by FINSEQ_1:def 3;
          i in Seg k by P12A,FINSEQ_1:1,P2;
          then
          P15: b.i = b1.i by FUNCT_1:49;
          P16: m.i = m1.i by FINSEQ_1:def 7,P13B;
          thus m.(i+1) = m.i * b.i by P13,FINSEQ_1:def 7,P13C,P15,P16;
        end;
      end;
      b|(k+1)=b1 ^ <*b.(len b)*> by INT_6:5,A2; then
      P17: b = b1^<* b.(len b )*> by FINSEQ_1:58,A2;
      len b in Seg (len m1) by FINSEQ_1:4,A2,P5B; then
      P18: len b in dom m1 by FINSEQ_1:def 3;
      P19: 1<=len b & len b <=len b by A2,NAT_1:12;
      Product b
      = m1.(len b1+1)*b.(len b ) by P4,RVSUM_1:96,P17
      .= m1.(len b )*b.(len b ) by A2,FINSEQ_1:59,NAT_1:12
      .= m.(len b)*b.(len b ) by FINSEQ_1:def 7,P18
      .= m.(len b + 1) by P9,P19;
      hence thesis by P5,P8,P9;
    end;
    for k be Element of NAT
    holds P[k] from NAT_1: sch 1(P0,P1);
    hence thesis;
  end;

theorem
  for nlist be non empty FinSequence of [:INT,INT:],
  a,b be non empty FinSequence of INT,
  x,y be Element of INT
  st len a = len b & len a = len nlist
  &
  (for i be Nat st i in Seg (len nlist)
  holds b.i <> 0 )

  &
  (for i be Nat st i in Seg (len nlist)
  holds
  (nlist.i)`1 = a.i & (nlist.i)`2 =b.i )
  &
  (for i,j be Nat st i in Seg (len nlist)
  & j in Seg (len nlist)
  & i <> j
  holds b.i,b.j are_relative_prime )
  &
  (for i be Nat st i in Seg (len nlist)
  holds x mod b.i = a.i mod b.i )
  & y = Product b
  holds ALGO_CRT(nlist) mod y = x mod y
  proof
    let nlist be non empty FinSequence of [:INT,INT:],
    a,b be non empty FinSequence of INT,
    x,y be Element of INT;
    assume A1:
    len a = len b & len a = len nlist;
    assume A2:
    for i be Nat st i in Seg (len nlist)
    holds b.i <> 0;
    assume A3:
    for i be Nat st i in Seg (len nlist)
    holds
    (nlist.i)`1 = a.i & (nlist.i)`2 = b.i;
    assume A4:
    for i,j be Nat st i in Seg (len nlist)
    & j in Seg (len nlist)
    & i <> j
    holds b.i,b.j are_relative_prime;
    assume A5:
    for i be Nat st i in Seg (len nlist)
    holds x mod b.i = a.i mod b.i;
    assume A6: y = Product b;
    P2: for i be Nat st i in Seg (len nlist)
    holds ALGO_CRT(nlist) mod b.i = x mod b.i
    proof
      let i be Nat;
      assume P21: i in Seg (len nlist);
      hence ALGO_CRT(nlist) mod b.i = a.i mod b.i by Th4,A1,A2,A3,A4
      .= x mod b.i by A5,P21;
    end;

    per cases;
    suppose P3: len nlist = 1;
      then
      P5: 1 in Seg(len nlist);
      thus
      ALGO_CRT(nlist) mod y
      = ALGO_CRT(nlist) mod b.1 by P3,A1,LmTh8,A6
      .= x mod b.1 by P2,P5
      .= x mod y by P3,A1,LmTh8,A6;
    end;
    suppose P4: len nlist <> 1;
      P5: 2 <= len nlist by P4,NAT_1:23;
      P6: 2 <= len b by A1,P4,NAT_1:23;
      consider m be non empty FinSequence of INT such that
      P7:
      len m = len b + 1 & m.1 = 1 &
      (for i be Nat st 1<=i & i <=len b holds
      m.(i+1) = m.i * b.i ) &
      Product b = m.(len b + 1) by LmTh9;
      1<= len b & len b <= len b by P6,XXREAL_0:2;
      hence ALGO_CRT(nlist) mod y = x mod y by A6,P7,LmTh7,A1,A4,P2,P5;
    end;
  end;