theorem :: FUNCT_7:65

for X being set
for x being object
for p being FuncSequence st x in firstdom p & x in X holds
(apply (p,x)) . ((len p) + 1) = (compose (p,X)) . x