for q being non empty non-empty FinSequence
for p being FuncSequence of q st p <> {} holds
( firstdom p = q . 1 & lastrng p c= q . (len q) )