theorem Th15: :: INTEGR23:13

for T being 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) ) )