for j, k being Nat
for D being non empty set
for p being FinSequence of D st len p = (j + 1) + k holds
ex q, r being FinSequence of D ex c being Element of D st
( len q = j & len r = k & p = (q ^ <*c*>) ^ r )