let v be FinSequence of REAL ; :: thesis: for n, m, i being Nat st v <> {} & rng v c= Seg n & 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 ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being 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, m, i be Nat; :: thesis: ( v <> {} & rng v c= Seg n & 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 ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being 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 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 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 Nat st k in dom v & v . k = i holds
k <= m ; :: thesis: ( m + 1 in dom v & v . (m + 1) = i + 1 )
A10: m <= len v by A7, FINSEQ_3:25;
0 + 1 <= len v by A1, NAT_1:13;
then A11: len v in dom v by FINSEQ_3:25;
reconsider r = v . (m + 1) as Real ;
A12: i <= n by A5, FINSEQ_1:1;
A13: 1 <= m by A7, FINSEQ_3:25;
A14: i + 1 <= n by A6, FINSEQ_1:1;

A15: now :: thesis: m + 1 in dom v

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

end;

then A17: m + 1 <= len v by FINSEQ_3:25;
then A18: m < len v by NAT_1:13;
A19: m <= (len v) - 1 by A17, XREAL_1:19;

now :: thesis: ( ( |.(i - r).| = 1 & m + 1 in dom v & v . (m + 1) = i + 1 ) or ( i = r & contradiction ) )

per cases ( |.(i - r).| = 1 or i = r ) by A4, A8, A13, A19;

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

now :: thesis: ( ( i > r & i = r + 1 & contradiction ) or ( i < r & r = i + 1 & m + 1 in dom v & v . (m + 1) = i + 1 ) )

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

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

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A23: S₁[k] ; :: thesis: S₁[k + 1]
let j be 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 that
A24: j = k + 1 and
A25: j > 0 and
A26: m + j in dom v and
A27: s = v . (m + j) ; :: thesis: s < i

now :: thesis: s < i

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

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

hence s < i by A21, A24, A27; :: thesis: verum

end;

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

A29: m + k <= (m + k) + 1 by NAT_1:11;
m <= m + k by NAT_1:11;
then A30: 1 <= m + k by A13, XXREAL_0:2;
A31: m + (k + 1) <= len v by A24, A26, FINSEQ_3:25;
then m + k <= len v by A29, XXREAL_0:2;
then A32: m + k in dom v by A30, 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 ;
A33: r1 < i by A23, A28, A32;
A34: m + k <= (len v) - 1 by A29, A31, XREAL_1:19;

now :: thesis: s < i

per cases ( |.(r1 - s).| = 1 or r1 = s ) by A4, A24, A27, A29, A30, A34;

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

now :: thesis: s < i

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

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

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

end;

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

then A36: s <= i by A33, NAT_1:13;

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

per cases ( s < i or s = i ) by A36, 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, A26, A27;
then j <= m - m by XREAL_1:19;
hence contradiction by A25; :: 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 A23, A28, A32; :: thesis: verum

end;

end;

end;

hence s < i ; :: thesis: verum

end;

end;

end;

hence s < i ; :: thesis: verum

end;

reconsider l = (len v) - m as Element of NAT by A18, INT_1:5;
A37: ( 0 < (len v) - m & m + l = len v ) by A17, XREAL_1:19;
A38: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A38, A22);
hence contradiction by A3, A11, A12, A37; :: 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 A15; :: 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, A15;
then 1 <= m - m by XREAL_1:19;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum

end;

end;

end;

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