for n being Nat
for p being XFinSequence st len p <= n holds
p | n = p