for p being non empty FinSequence
for q being FinSequence
for i being Nat st i < len q holds
(p $^ q) . ((len p) + i) = q . (i + 1)