let T be FinSequence of REAL ; for n, m being Nat st n + 1 < m & m <= len T holds
ex TM1 being 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 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 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) ) )
deffunc H1( Nat) -> set = T . ($1 + n);
m - (n + 1) in NAT
by A1, INT_1:5;
then reconsider m1 = m - (n + 1) as Nat ;
consider p being FinSequence such that
A2:
( len p = m1 & ( for k being Nat st k in dom p holds
p . k = H1(k) ) )
from FINSEQ_1:sch 2();
A3:
rng p c= rng T
proof
let x be
object ;
TARSKI:def 3 ( not x in rng p or x in rng T )
assume
x in rng p
;
x in rng T
then consider i being
object such that A4:
(
i in dom p &
x = p . i )
by FUNCT_1:def 3;
reconsider i =
i as
Nat by A4;
A6:
p . i = T . (i + n)
by A2, A4;
A7:
( 1
<= i &
i <= m1 )
by A2, FINSEQ_3:25, A4;
A8:
i + n <= m1 + n
by A7, XREAL_1:6;
m - 1
<= m - 0
by XREAL_1:10;
then
m - 1
<= len T
by A1, XXREAL_0:2;
then A9:
i + n <= len T
by A8, XXREAL_0:2;
1
+ 0 <= i + n
by A7, XREAL_1:7;
then
i + n in dom T
by FINSEQ_3:25, A9;
hence
x in rng T
by A4, A6, FUNCT_1:3;
verum
end;
then reconsider p = p as FinSequence of REAL by FINSEQ_1:def 4, XBOOLE_1:1;
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)
by A2; ( rng p c= rng T & ( for i being Nat st i in dom p holds
p . i = T . (i + n) ) )
thus
rng p c= rng T
by A3; for i being Nat st i in dom p holds
p . i = T . (i + n)
let i be Nat; ( i in dom p implies p . i = T . (i + n) )
assume
i in dom p
; p . i = T . (i + n)
hence
p . i = T . (i + n)
by A2; verum