theorem Th4: :: SPRECT_2:4

for i, j, k being Nat
for D being non empty set
for f being FinSequence of D st i > j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds
(mid (f,i,j)) /. k = f /. ((i -' k) + 1)