theorem Th18: :: HILBERT3:19

for f being Function-yielding Function
for g, h being Function st dom f = dom g holds
(f .. g) * h = (f * h) .. (g * h)