theorem Th9: :: SPRECT_2:9

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
(mid (f,i,j)) /. (len (mid (f,i,j))) = f /. j