theorem Th8: :: GLIBPRE1:8

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