theorem Th1: :: SPRECT_2:1

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
(k + i) -' 1 in dom f