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