theorem Th17: :: INTEGR23:15

for p being FinSequence of REAL
for n, m being Nat st n + 1 < m & m <= len p holds
ex pM1 being FinSequence of REAL st
( len pM1 = (m - (n + 1)) - 1 & rng pM1 c= rng p & ( for i being Nat st i in dom pM1 holds
pM1 . i = p . ((i + n) + 1) ) )