theorem Th9: :: FINSEQ_8:9

for f, g being FinSequence holds smid ((f ^ g),((len f) + 1),((len f) + (len g))) = g