theorem :: FUNCT_7:44

for x being object
for p being Function-yielding FinSequence
for f being Function holds apply ((<*f*> ^ p),x) = <*x*> ^ (apply (p,(f . x)))