theorem Th7: :: SPRECT_2:7

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
not mid (f,i,j) is empty