theorem :: FUNCT_7:48

for X, Y being set
for p, q being Function-yielding FinSequence st rng (compose (p,X)) c= Y holds
compose ((p ^ q),X) = (compose (q,Y)) * (compose (p,X))