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