let p be FinSequence of REAL ; 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 ; ( 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
; 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; verum