theorem Th10: :: FUNCT_7:10

for f, g, h being Function holds (g +* h) * f = (g * f) +* (h * f)