theorem Th5: :: SPRECT_2:5

for i, j being Nat
for D being non empty set
for f being FinSequence of D st i in dom f & j in dom f holds
len (mid (f,i,j)) >= 1