for i, j being natural Number
for r being FinSequence st len r = i + j holds
ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q )