let p be FinSequence of REAL ; :: thesis: for i, j, k being Element of NAT st p is increasing & i in dom p & j in dom p & k in dom p & p . i <= p . k & p . k <= p . j holds
p . k in rng (mid (p,i,j))

let i, j, k be Element of NAT ; :: thesis: ( p is increasing & i in dom p & j in dom p & k in dom p & p . i <= p . k & p . k <= p . j implies p . k in rng (mid (p,i,j)) )
assume that
A1: p is increasing and
A2: i in dom p and
A3: j in dom p and
A4: k in dom p and
A5: p . i <= p . k and
A6: p . k <= p . j ; :: thesis: p . k in rng (mid (p,i,j))
A7: 1 <= i by ;
A8: 1 <= j by ;
A9: j <= len p by ;
A10: i <= k by ;
then consider n being Nat such that
A11: k + 1 = i + n by ;
A12: k <= j by ;
then k - i <= j - i by XREAL_1:9;
then A13: (k - i) + 1 <= (j - i) + 1 by XREAL_1:6;
k - i >= 0 by ;
then A14: (k - i) + 1 >= 0 + 1 by XREAL_1:6;
A15: i <= j by ;
i <= len p by ;
then len (mid (p,i,j)) = (j -' i) + 1 by ;
then len (mid (p,i,j)) = (j - i) + 1 by ;
then A16: n in dom (mid (p,i,j)) by ;
(mid (p,i,j)) . n = p . ((n + i) - 1) by
.= p . k by A11 ;
hence p . k in rng (mid (p,i,j)) by ; :: thesis: verum