let T be non empty increasing FinSequence of REAL ; :: thesis: for n, m being Nat st n + 1 < m & m <= len T holds
ex TM1 being non empty increasing FinSequence of REAL st
( len TM1 = m - (n + 1) & rng TM1 c= rng T & ( for i being Nat st i in dom TM1 holds
TM1 . i = T . (i + n) ) )
let n, m be Nat; :: thesis: ( n + 1 < m & m <= len T implies ex TM1 being non empty increasing FinSequence of REAL st
( len TM1 = m - (n + 1) & rng TM1 c= rng T & ( for i being Nat st i in dom TM1 holds
TM1 . i = T . (i + n) ) ) )
assume A1: ( n + 1 < m & m <= len T ) ; :: thesis: ex TM1 being non empty increasing FinSequence of REAL st
( len TM1 = m - (n + 1) & rng TM1 c= rng T & ( for i being Nat st i in dom TM1 holds
TM1 . i = T . (i + n) ) )
then consider p being FinSequence of REAL such that
A2: ( len p = m - (n + 1) & rng p c= rng T & ( for i being Nat st i in dom p holds
p . i = T . (i + n) ) ) by Th15;
m - (n + 1) in NAT by A1, INT_1:5;
then reconsider m1 = m - (n + 1) as Nat ;
len p <> 0 by A1, A2;
then reconsider p = p as non empty FinSequence of REAL ;
for e1, e2 being ExtReal st e1 in dom p & e2 in dom p & e1 < e2 holds
p . e1 < p . e2

proof

let e1, e2 be ExtReal; :: thesis: ( e1 in dom p & e2 in dom p & e1 < e2 implies p . e1 < p . e2 )
assume A3: ( e1 in dom p & e2 in dom p & e1 < e2 ) ; :: thesis: p . e1 < p . e2
then reconsider ie1 = e1, ie2 = e2 as Nat ;
A5: p . e1 = T . (ie1 + n) by A2, A3;
A6: p . e2 = T . (ie2 + n) by A2, A3;
A7: ( 1 <= ie1 & ie1 <= m1 ) by A2, A3, FINSEQ_3:25;
A8: ( 1 <= ie2 & ie2 <= m1 ) by A2, A3, FINSEQ_3:25;
A9: ie1 + n <= m1 + n by A7, XREAL_1:6;
m - 1 <= m - 0 by XREAL_1:10;
then A10: m - 1 <= len T by A1, XXREAL_0:2;
then A11: ie1 + n <= len T by A9, XXREAL_0:2;
1 + 0 <= ie1 + n by A7, XREAL_1:7;
then A12: ie1 + n in dom T by A11, FINSEQ_3:25;
A13: 1 + 0 <= ie2 + n by A8, XREAL_1:7;
ie2 + n <= m1 + n by A8, XREAL_1:6;
then ie2 + n <= len T by A10, XXREAL_0:2;
then A14: ie2 + n in dom T by FINSEQ_3:25, A13;
ie1 + n < ie2 + n by A3, XREAL_1:8;
hence p . e1 < p . e2 by A5, A6, A12, A14, VALUED_0:def 13; :: thesis: verum

end;

then reconsider p = p as non empty increasing FinSequence of REAL by VALUED_0:def 13;
take p ; :: thesis: ( len p = m - (n + 1) & rng p c= rng T & ( for i being Nat st i in dom p holds
p . i = T . (i + n) ) )
thus ( len p = m - (n + 1) & rng p c= rng T & ( for i being Nat st i in dom p holds
p . i = T . (i + n) ) ) by A2; :: thesis: verum