theorem Th5: :: FINSEQ_8:5

for D being non empty set
for f being FinSequence of D
for k2 being Element of NAT holds smid (f,1,k2) = f | k2