theorem Th7: :: FINSEQ_8:7

for D being set
for f being FinSequence of D
for k1, k2 being Element of NAT st k1 > k2 holds
smid (f,k1,k2) = {}