theorem Th12: :: FUNCTOR0:12

for F, G being Function-yielding Function
for f being Function holds (G ** F) * f = (G * f) ** (F * f)