theorem Th2: :: SPRECT_2:2

for i, j, k being Nat
for D being non empty set
for f being FinSequence of D st i > j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds
(i -' k) + 1 in dom f