let v be FinSequence of REAL ; :: thesis: for n, i, m being Element of NAT st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being Element of NAT st k in dom v & v . k = i holds
k <= m ) holds
( m + 1 in dom v & v . (m + 1) = i + 1 )
let n, i, m be Element of NAT ; :: thesis: ( v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being Element of NAT st k in dom v & v . k = i holds
k <= m ) implies ( m + 1 in dom v & v . (m + 1) = i + 1 ) )
assume that
A1: v <> {} and
A2: rng v c= Seg n and
A3: v . (len v) = n and
A4: for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s and
A5: i in Seg n and
A6: i + 1 in Seg n and
A7: m in dom v and
A8: v . m = i and
A9: for k being Element of NAT st k in dom v & v . k = i holds
k <= m ; :: thesis: ( m + 1 in dom v & v . (m + 1) = i + 1 )
len v <> 0 by A1;
then 0 < len v ;
then ( 0 + 1 <= len v & len v <= len v ) by NAT_1:13;
then A10: len v in dom v by FINSEQ_3:27;
A11: ( 1 <= i & i <= n & 1 <= i + 1 & i + 1 <= n ) by A5, A6, FINSEQ_1:3;
A12: ( 1 <= m & m <= len v & m <= m + 1 ) by A7, FINSEQ_3:27, NAT_1:11;

A13: now

assume not m + 1 in dom v ; :: thesis: contradiction
then ( 1 > m + 1 or m + 1 > len v ) by FINSEQ_3:27;
then ( len v <= m & i < n ) by A11, NAT_1:11, NAT_1:13;
hence contradiction by A3, A8, A12, XXREAL_0:1; :: thesis: verum

end;

reconsider r = v . (m + 1) as Real ;
A14: m + 1 <= len v by A13, FINSEQ_3:27;
then A15: ( m <= (len v) - 1 & m < len v ) by NAT_1:13, XREAL_1:21;

now

per cases ( abs (i - r) = 1 or i = r ) by A4, A8, A12, A15;

case A16: abs (i - r) = 1 ; :: thesis: ( m + 1 in dom v & v . (m + 1) = i + 1 )

now

per cases ( ( i > r & i = r + 1 ) or ( i < r & r = i + 1 ) ) by A16, Th1;

case A17: ( i > r & i = r + 1 ) ; :: thesis: contradiction

defpred S₁[ set ] means for k being Element of NAT
for r being Real st k = $1 & k > 0 & m + k in dom v & r = v . (m + k) holds
r < i;
A18: S₁[ 0 ] ;
A19: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A20: S₁[k] ; :: thesis: S₁[k + 1]
let j be Element of NAT ; :: thesis: for r being Real st j = k + 1 & j > 0 & m + j in dom v & r = v . (m + j) holds
r < i
let s be Real; :: thesis: ( j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) implies s < i )
assume A21: ( j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) ) ; :: thesis: s < i

now

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

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

hence s < i by A17, A21; :: thesis: verum

end;

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

then A22: ( 0 < k & m <= m + k & m + k <= (m + k) + 1 & (m + k) + 1 = m + (k + 1) ) by NAT_1:11;
then A23: ( 1 <= m + k & m + (k + 1) <= len v ) by A12, A21, FINSEQ_3:27, XXREAL_0:2;
then ( 1 <= m + k & m + k <= len v ) by A22, XXREAL_0:2;
then A24: m + k in dom v by FINSEQ_3:27;
then v . (m + k) in rng v by FUNCT_1:def 5;
then ( v . (m + k) in Seg n & Seg n c= NAT ) by A2;
then reconsider r1 = v . (m + k) as Element of NAT ;
A25: r1 < i by A20, A22, A24;
A26: m + k <= (len v) - 1 by A22, A23, XREAL_1:21;

now

per cases ( abs (r1 - s) = 1 or r1 = s ) by A4, A21, A22, A23, A26;

suppose A27: abs (r1 - s) = 1 ; :: thesis: s < i

now

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

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

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

end;

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

then A28: s <= i by A25, NAT_1:13;

now

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

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

hence s < i ; :: thesis: verum

end;

case s = i ; :: thesis: contradiction

then m + j <= m by A9, A21;
then j <= m - m by XREAL_1:21;
hence contradiction by A21; :: thesis: verum

end;

end;

end;

hence s < i ; :: thesis: verum

end;

end;

end;

hence s < i ; :: thesis: verum

end;

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

hence s < i by A20, A22, A24; :: thesis: verum

end;

end;

end;

hence s < i ; :: thesis: verum

end;

end;

end;

hence s < i ; :: thesis: verum

end;

A29: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A18, A19);
A30: 0 < (len v) - m by A14, XREAL_1:21;
reconsider l = (len v) - m as Element of NAT by A15, INT_1:18;
m + l = len v ;
hence contradiction by A3, A10, A11, A29, A30; :: thesis: verum

end;

case ( i < r & r = i + 1 ) ; :: thesis: ( m + 1 in dom v & v . (m + 1) = i + 1 )

hence ( m + 1 in dom v & v . (m + 1) = i + 1 ) by A13; :: thesis: verum

end;

end;

end;

hence ( m + 1 in dom v & v . (m + 1) = i + 1 ) ; :: thesis: verum

end;

case i = r ; :: thesis: contradiction

then m + 1 <= m by A9, A13;
then 1 <= m - m by XREAL_1:21;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence ( m + 1 in dom v & v . (m + 1) = i + 1 ) ; :: thesis: verum