theorem Th16: :: INTEGR23:14

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