theorem Th4: :: FINSEQ_8:4

for f being FinSequence
for k1, k2 being Element of NAT st k1 <= k2 holds
smid (f,k1,k2) = mid (f,k1,k2)