theorem Th41: :: FUNCT_7:42

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