theorem Th6: :: FINSEQ_8:6

for f being FinSequence
for k2 being Nat st len f <= k2 holds
smid (f,1,k2) = f