let s1, s2 be Element of INT ; :: thesis: ( ( len nlist = 1 implies s1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s1 = (n . (len m)) mod M ) ) & ( len nlist = 1 implies s2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s2 = (n . (len m)) mod M ) ) implies s1 = s2 )
assume A30: ( ( len nlist = 1 implies s1 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s1 = (n . (len m)) mod M ) ) ) ; :: thesis: ( ( len nlist = 1 & not s2 = (nlist . 1) `1 ) or ( len nlist <> 1 & ( for m, n, prodc, prodi being FinSequence of INT
for M0, M being Element of INT holds
( not len m = len nlist or not len n = len nlist or not len prodc = (len nlist) - 1 or not len prodi = (len nlist) - 1 or not m . 1 = 1 or ex i being Nat st
( 1 <= i & i <= (len m) - 1 & ( for d, x, y being Element of INT holds
( not x = (nlist . i) `2 or not m . (i + 1) = (m . i) * x or not y = m . (i + 1) or not d = (nlist . (i + 1)) `2 or not prodi . i = ALGO_INVERSE (y,d) or not prodc . i = y ) ) ) or not M0 = (nlist . (len m)) `2 or not M = (prodc . ((len m) - 1)) * M0 or not n . 1 = (nlist . 1) `1 or ex i being Nat st
( 1 <= i & i <= (len m) - 1 & ( for u, u0, u1 being Element of INT holds
( not u0 = (nlist . (i + 1)) `1 or not u1 = (nlist . (i + 1)) `2 or not u = ((u0 - (n . i)) * (prodi . i)) mod u1 or not n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) ) or not s2 = (n . (len m)) mod M ) ) ) or s1 = s2 )
assume A31: ( ( len nlist = 1 implies s2 = (nlist . 1) `1 ) & ( len nlist <> 1 implies ex m, n, prodc, prodi being FinSequence of INT ex M0, M being Element of INT st
( len m = len nlist & len n = len nlist & len prodc = (len nlist) - 1 & len prodi = (len nlist) - 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex d, x, y being Element of INT st
( x = (nlist . i) `2 & m . (i + 1) = (m . i) * x & y = m . (i + 1) & d = (nlist . (i + 1)) `2 & prodi . i = ALGO_INVERSE (y,d) & prodc . i = y ) ) & M0 = (nlist . (len m)) `2 & M = (prodc . ((len m) - 1)) * M0 & n . 1 = (nlist . 1) `1 & ( for i being Nat st 1 <= i & i <= (len m) - 1 holds
ex u, u0, u1 being Element of INT st
( u0 = (nlist . (i + 1)) `1 & u1 = (nlist . (i + 1)) `2 & u = ((u0 - (n . i)) * (prodi . i)) mod u1 & n . (i + 1) = (n . i) + (u * (prodc . i)) ) ) & s2 = (n . (len m)) mod M ) ) ) ; :: thesis: s1 = s2

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

suppose len nlist = 1 ; :: thesis: s1 = s2

hence s1 = s2 by A30, A31; :: thesis: verum

end;

suppose A33: len nlist <> 1 ; :: thesis: s1 = s2

consider m1, n1, prodc1, prodi1 being FinSequence of INT , M01, M1 being Element of INT such that
A34: ( len m1 = len nlist & len n1 = len nlist & len prodc1 = (len nlist) - 1 & len prodi1 = (len nlist) - 1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m1) - 1 holds
ex d, x, y being 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 being Nat st 1 <= i & i <= (len m1) - 1 holds
ex u, u0, u1 being 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 A33, A30;
consider m2, n2, prodc2, prodi2 being FinSequence of INT , M02, M2 being Element of INT such that
A35: ( len m2 = len nlist & len n2 = len nlist & len prodc2 = (len nlist) - 1 & len prodi2 = (len nlist) - 1 & m2 . 1 = 1 & ( for i being Nat st 1 <= i & i <= (len m2) - 1 holds
ex d, x, y being 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 being Nat st 1 <= i & i <= (len m2) - 1 holds
ex u, u0, u1 being 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 A33, A31;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len m1 implies m1 . $1 = m2 . $1 );
A36: S₁[ 0 ] ;
A37: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A38: S₁[i] ; :: thesis: S₁[i + 1]
assume ( 1 <= i + 1 & i + 1 <= len m1 ) ; :: thesis: m1 . (i + 1) = m2 . (i + 1)
then A39: ( 1 - 1 <= (i + 1) - 1 & (i + 1) - 1 <= (len m1) - 1 ) by XREAL_1:9;
A40: (len m1) - 1 <= (len m1) - 0 by XREAL_1:13;

per cases ( i = 0 or i <> 0 ) ;

suppose A41: i = 0 ; :: thesis: m1 . (i + 1) = m2 . (i + 1)

thus m1 . (i + 1) = m2 . (i + 1) by A34, A35, A41; :: thesis: verum

end;

suppose A42: i <> 0 ; :: thesis: m1 . (i + 1) = m2 . (i + 1)

then A43: 1 <= i by NAT_1:14;
A44: ex d, x, y being 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 A34, A43, A39;
( 1 <= i & i <= (len m2) - 1 ) by A42, A39, A34, A35, NAT_1:14;
then ex d, x, y being 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 A35;
hence m1 . (i + 1) = m2 . (i + 1) by A44, A39, A38, A40, A42, NAT_1:14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A45: for k being Nat holds S₁[k] from NAT_1:sch 2(A36, A37);

A46: now :: thesis: for i being Nat st 1 <= i & i <= len prodc1 holds
prodc1 . i = prodc2 . i

let i be Nat; :: thesis: ( 1 <= i & i <= len prodc1 implies prodc1 . i = prodc2 . i )
assume A47: ( 1 <= i & i <= len prodc1 ) ; :: thesis: prodc1 . i = prodc2 . i
then A48: ex d, x, y being 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 A34;
ex d, x, y being 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 A35, A47, A34;
hence prodc1 . i = prodc2 . i by A48, A34, A35, A45, FINSEQ_1:14; :: thesis: verum

end;

then A49: prodc1 = prodc2 by A34, A35;

A50: now :: thesis: for i being Nat st 1 <= i & i <= len prodi1 holds
prodi1 . i = prodi2 . i

let i be Nat; :: thesis: ( 1 <= i & i <= len prodi1 implies prodi1 . i = prodi2 . i )
assume A51: ( 1 <= i & i <= len prodi1 ) ; :: thesis: prodi1 . i = prodi2 . i
then A52: ex d, x, y being 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 A34;
ex d, x, y being 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 A35, A51, A34;
hence prodi1 . i = prodi2 . i by A52, A45, A34, A35, FINSEQ_1:14; :: thesis: verum

end;

A53: M1 = M2 by A35, A34, A46, FINSEQ_1:14;
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= len n1 implies n1 . $1 = n2 . $1 );
A54: S₂[ 0 ] ;
A55: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A56: S₂[k] ; :: thesis: S₂[k + 1]
assume ( 1 <= k + 1 & k + 1 <= len n1 ) ; :: thesis: n1 . (k + 1) = n2 . (k + 1)
then A57: ( 1 - 1 <= (k + 1) - 1 & (k + 1) - 1 <= (len n1) - 1 ) by XREAL_1:9;
A58: (len n1) - 1 <= (len n1) - 0 by XREAL_1:13;

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: n1 . (k + 1) = n2 . (k + 1)

hence n1 . (k + 1) = n2 . (k + 1) by A34, A35; :: thesis: verum

end;

suppose A60: k <> 0 ; :: thesis: n1 . (k + 1) = n2 . (k + 1)

then A61: 1 <= k by NAT_1:14;
A62: ex u, u0, u1 being 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 A61, A57, A34;
ex u, u0, u1 being 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 A61, A57, A34, A35;
hence n1 . (k + 1) = n2 . (k + 1) by A49, A62, A56, A58, A60, A57, A34, A35, A50, FINSEQ_1:14, NAT_1:14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A54, A55);
hence s1 = s2 by A53, A34, A35, FINSEQ_1:14; :: thesis: verum

end;

end;