for k, n being Nat
for p being XFinSequence st len p = n + k holds
ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 )