theorem :: FINSEQ_8:8

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