for n being Nat
for p being XFinSequence st n >= len p holds
p /^ n = {}