for p, q being FinSequence st q <> {} holds
(len (p ^' q)) + 1 = (len p) + (len q)