theorem :: FINSEQ_8:1

for f, g being FinSequence st len f >= 1 holds
mid ((f ^ g),1,(len f)) = f