theorem :: FUNCT_7:67

for q being non empty non-empty FinSequence
for p being FuncSequence of q holds
( dom (compose (p,(q . 1))) = q . 1 & rng (compose (p,(q . 1))) c= q . (len q) )