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 ; :: 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 ;
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 ;
defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len m1 implies m1 . \$1 = m2 . \$1 );
A36: S1[ 0 ] ;
A37: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A38: S1[i] ; :: thesis: S1[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 ; :: 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 ;
( 1 <= i & i <= (len m2) - 1 ) by ;
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 ; :: thesis: verum
end;
end;
end;
A45: for k being Nat holds S1[k] from
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 ;
hence prodc1 . i = prodc2 . i by ; :: thesis: verum
end;
then A49: prodc1 = prodc2 by ;
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 ;
hence prodi1 . i = prodi2 . i by ; :: thesis: verum
end;
A53: M1 = M2 by ;
defpred S2[ Nat] means ( 1 <= \$1 & \$1 <= len n1 implies n1 . \$1 = n2 . \$1 );
A54: S2[ 0 ] ;
A55: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A56: S2[k] ; :: thesis: S2[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 ; :: 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 ;
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 ; :: thesis: verum
end;
end;
end;
for k being Nat holds S2[k] from hence s1 = s2 by ; :: thesis: verum
end;
end;