theorem :: FINSEQ_8:8

for D being set
for f being FinSequence of D
for k2 being Element of NAT holds smid (f,0,k2) = smid (f,1,(k2 + 1))