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