theorem Th7: :: FINSEQ_8:7

for f being FinSequence
for k1, k2 being Nat st k1 > k2 holds
smid (f,k1,k2) = {}