theorem Th40: :: FUNCT_7:41

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