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