let T be non empty increasing FinSequence of REAL ; 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; ( 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 )
; 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;
( 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 )
;
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;
verum
end;
then reconsider p = p as non empty increasing FinSequence of REAL by VALUED_0:def 13;
take
p
; ( 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; verum