theorem Th9: :: FUNCT_7:9

for f, g, h being Function st rng h c= dom f holds
f * (g +* h) = (f * g) +* (f * h)