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

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