theorem Th6: :: SPRECT_2:6

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 & len (mid (f,i,j)) = 1 holds
i = j