theorem :: FUNCT_7:50

for x being object
for p, q being Function-yielding FinSequence holds apply ((p ^ q),x) = (apply (p,x)) $^ (apply (q,((apply (p,x)) . ((len p) + 1))))