theorem Th9: :: FINSEQ_8:9

for D being non empty set
for f, g being FinSequence of D holds smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g