theorem Th8: :: SPRECT_2:8

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)) /. 1 = f /. i