theorem Th48: :: FUNCT_7:49

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