theorem Th5: :: FINSEQ_8:5

for f being FinSequence
for k2 being Nat holds smid (f,1,k2) = f | k2