theorem Th5: :: FILEREC1:5

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