for D being set
for f, g being FinSequence of D holds (f ^' g) | (len f) = f