theorem :: FUNCT_7:43

for X being set
for p being Function-yielding FinSequence
for f being Function holds compose ((<*f*> ^ p),X) = (compose (p,(f .: X))) * (f | X)