for n being Nat
for p being XFinSequence st n < len p holds
len (p /^ n) = (len p) - n