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 A2, FINSEQ_3:25;
A8: 1 <= j by A3, FINSEQ_3:25;
A9: j <= len p by A3, FINSEQ_3:25;
A10: i <= k by A1, A2, A4, A5, SEQM_3:def 1;
then consider n being Nat such that
A11: k + 1 = i + n by NAT_1:10, NAT_1:12;
A12: k <= j by A1, A3, A4, A6, SEQM_3:def 1;
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 A10, XREAL_1:48;
then A14: (k - i) + 1 >= 0 + 1 by XREAL_1:6;
A15: i <= j by A10, A12, XXREAL_0:2;
i <= len p by A2, FINSEQ_3:25;
then len (mid (p,i,j)) = (j -' i) + 1 by A7, A8, A9, A15, FINSEQ_6:118;
then len (mid (p,i,j)) = (j - i) + 1 by A10, A12, XREAL_1:233, XXREAL_0:2;
then A16: n in dom (mid (p,i,j)) by A11, A14, A13, FINSEQ_3:25;
(mid (p,i,j)) . n = p . ((n + i) - 1) by A7, A9, A15, A11, A14, A13, FINSEQ_6:122
.= p . k by A11 ;
hence p . k in rng (mid (p,i,j)) by A16, FUNCT_1:def 3; :: thesis: verum