theorem Th4: :: FINSEQ_8:4

for f being FinSequence
for k1, k2 being Nat st k1 <= k2 holds
smid (f,k1,k2) = mid (f,k1,k2)