let v be FinSequence of REAL ; :: thesis: for n being Nat st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Nat st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds
r = s ) holds
( ( for i being Nat st i in Seg n holds
ex k being Nat st
( k in dom v & v . k = i ) ) & ( for m, k, i being Nat
for r being Real st m in dom v & v . m = i & ( for j being Nat st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) )
let n be Nat; :: thesis: ( v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Nat st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds
r = s ) implies ( ( for i being Nat st i in Seg n holds
ex k being Nat st
( k in dom v & v . k = i ) ) & ( for m, k, i being Nat
for r being Real st m in dom v & v . m = i & ( for j being Nat st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) ) )
assume that
A1: v <> {} and
A2: rng v c= Seg n and
A3: v . 1 = 1 and
A4: v . (len v) = n and
A5: for k being Nat st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds
r = s ; :: thesis: ( ( for i being Nat st i in Seg n holds
ex k being Nat st
( k in dom v & v . k = i ) ) & ( for m, k, i being Nat
for r being Real st m in dom v & v . m = i & ( for j being Nat st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) )
defpred S₁[ Nat] means ( $1 in Seg n implies ex k being Nat st
( k in dom v & v . k = $1 ) );
A6: 0 + 1 <= len v by A1, NAT_1:13;
then A7: len v in dom v by FINSEQ_3:25;
A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A9: ( i in Seg n implies ex k being Nat st
( k in dom v & v . k = i ) ) ; :: thesis: S₁[i + 1]
assume A10: i + 1 in Seg n ; :: thesis: ex k being Nat st
( k in dom v & v . k = i + 1 )

now :: thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )

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

suppose A11: i = 0 ; :: thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )

take k = 1; :: thesis: ( k in dom v & v . k = i + 1 )
thus ( k in dom v & v . k = i + 1 ) by A3, A6, A11, FINSEQ_3:25; :: thesis: verum

end;

suppose A12: i <> 0 ; :: thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )

defpred S₂[ set ] means ( $1 in dom v & v . $1 = i );
A13: for k being Nat st S₂[k] holds
k <= len v by FINSEQ_3:25;
i + 1 <= n by A10, FINSEQ_1:1;
then A14: i <= n by NAT_1:13;
A15: 0 + 1 <= i by A12, NAT_1:13;
then A16: ex k being Nat st S₂[k] by A9, A14, FINSEQ_1:1;
consider m being Nat such that
A17: ( S₂[m] & ( for k being Nat st S₂[k] holds
k <= m ) ) from NAT_1:sch 6(A13, A16);
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take k = m + 1; :: thesis: ( k in dom v & v . k = i + 1 )
i in Seg n by A15, A14, FINSEQ_1:1;
hence ( k in dom v & v . k = i + 1 ) by A1, A2, A4, A5, A10, A17, Th44; :: thesis: verum

end;

end;

end;

hence ex k being Nat st
( k in dom v & v . k = i + 1 ) ; :: thesis: verum

end;

A18: S₁[ 0 ] by FINSEQ_1:1;
thus for i being Nat holds S₁[i] from NAT_1:sch 2(A18, A8); :: thesis: for m, k, i being Nat
for r being Real st m in dom v & v . m = i & ( for j being Nat st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r
let m, k, i be Nat; :: thesis: for r being Real st m in dom v & v . m = i & ( for j being Nat st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r
let r be Real; :: thesis: ( m in dom v & v . m = i & ( for j being Nat st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k implies i < r )
assume that
A19: m in dom v and
A20: v . m = i and
A21: for j being Nat st j in dom v & v . j = i holds
j <= m and
A22: m < k and
A23: k in dom v and
A24: r = v . k ; :: thesis: i < r
A25: ( m <= len v & k <= len v ) by A19, A23, FINSEQ_3:25;
A26: 1 <= m by A19, FINSEQ_3:25;
A27: i in rng v by A19, A20, FUNCT_1:def 3;
then A28: i <= n by A2, FINSEQ_1:1;

now :: thesis: i < r

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

suppose i = n ; :: thesis: i < r

then len v <= m by A4, A7, A21;
hence i < r by A22, A25, XXREAL_0:1; :: thesis: verum

end;

suppose A29: i <> n ; :: thesis: i < r

defpred S₂[ set ] means for j being Nat
for s being Real st j = $1 & j > 0 & m + j in dom v & s = v . (m + j) holds
i < s;
i < n by A28, A29, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then i + 1 in Seg n by FINSEQ_1:1;
then A30: v . (m + 1) = i + 1 by A1, A2, A4, A5, A19, A20, A21, A27, Th44;
A31: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A32: S₂[k] ; :: thesis: S₂[k + 1]
let j be Nat; :: thesis: for s being Real st j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) holds
i < s
let s be Real; :: thesis: ( j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) implies i < s )
assume that
A33: j = k + 1 and
A34: j > 0 and
A35: m + j in dom v and
A36: s = v . (m + j) ; :: thesis: i < s

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

suppose k = 0 ; :: thesis: i < s

hence i < s by A30, A33, A36, NAT_1:13; :: thesis: verum

end;

suppose A37: k <> 0 ; :: thesis: i < s

m <= m + k by NAT_1:11;
then A38: 1 <= m + k by A26, XXREAL_0:2;
s in rng v by A35, A36, FUNCT_1:def 3;
then s in Seg n by A2;
then reconsider s1 = s as Element of NAT ;
A39: m + (k + 1) <= len v by A33, A35, FINSEQ_3:25;
m + k <= (m + k) + 1 by NAT_1:11;
then m + k <= len v by A39, XXREAL_0:2;
then A40: m + k in dom v by A38, FINSEQ_3:25;
then v . (m + k) in rng v by FUNCT_1:def 3;
then v . (m + k) in Seg n by A2;
then reconsider r1 = v . (m + k) as Element of NAT ;
A41: i < r1 by A32, A37, A40;
A42: (m + k) + 1 = m + (k + 1) ;
then A43: m + k <= (len v) - 1 by A39, XREAL_1:19;

now :: thesis: i < s

per cases ( |.(r1 - s).| = 1 or r1 = s ) by A5, A33, A36, A42, A38, A43;

suppose A44: |.(r1 - s).| = 1 ; :: thesis: i < s

now :: thesis: i < s

per cases ( ( r1 > s & r1 = s + 1 ) or ( r1 < s & s = r1 + 1 ) ) by A44, Th40;

suppose ( r1 > s & r1 = s + 1 ) ; :: thesis: i < s

then A45: i <= s1 by A41, NAT_1:13;

now :: thesis: ( ( i < s & i < s ) or ( s = i & contradiction ) )

per cases ( i < s or s = i ) by A45, XXREAL_0:1;

case i < s ; :: thesis: i < s

hence i < s ; :: thesis: verum

end;

case s = i ; :: thesis: contradiction

then m + j <= m by A21, A35, A36;
then j <= m - m by XREAL_1:19;
hence contradiction by A34; :: thesis: verum

end;

end;

end;

hence i < s ; :: thesis: verum

end;

suppose ( r1 < s & s = r1 + 1 ) ; :: thesis: i < s

hence i < s by A41, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence i < s ; :: thesis: verum

end;

suppose r1 = s ; :: thesis: i < s

hence i < s by A32, A37, A40; :: thesis: verum

end;

end;

end;

hence i < s ; :: thesis: verum

end;

end;

end;

reconsider l = k - m as Element of NAT by A22, INT_1:5;
A46: ( 0 < k - m & m + l = k ) by A22, XREAL_1:50;
A47: S₂[ 0 ] ;
for k being Nat holds S₂[k] from NAT_1:sch 2(A47, A31);
hence i < r by A23, A24, A46; :: thesis: verum

end;

end;

end;

hence i < r ; :: thesis: verum