for a being natural Number
for D being set
for p being FinSequence of D holds p | (Seg a) is FinSequence of D