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 & i <= len p ) by A2, FINSEQ_3:27;
A8: ( 1 <= j & j <= len p ) by A3, FINSEQ_3:27;
A9: i <= k by A1, A2, A4, A5, SEQM_3:def 1;
A10: k <= j by A1, A3, A4, A6, SEQM_3:def 1;
then A11: i <= j by A9, XXREAL_0:2;
then len (mid p,i,j) = (j -' i) + 1 by A7, A8, JORDAN3:27;
then A12: len (mid p,i,j) = (j - i) + 1 by A9, A10, XREAL_1:235, XXREAL_0:2;
i <= k + 1 by A9, NAT_1:12;
then consider n being Nat such that
A13: k + 1 = i + n by NAT_1:10;
k - i >= 0 by A9, XREAL_1:50;
then A14: (k - i) + 1 >= 0 + 1 by XREAL_1:8;
k - i <= j - i by A10, XREAL_1:11;
then A15: (k - i) + 1 <= (j - i) + 1 by XREAL_1:8;
then A16: n in dom (mid p,i,j) by A12, A13, A14, FINSEQ_3:27;
n in NAT by ORDINAL1:def 13;
then (mid p,i,j) . n = p . ((n + i) - 1) by A7, A8, A11, A13, A14, A15, JORDAN3:31
.= p . k by A13 ;
hence p . k in rng (mid p,i,j) by A16, FUNCT_1:def 5; :: thesis: verum