theorem Th34: :: FUNCOP_1:34
for f, h, F being Function
for x being object holds (F [;] (x,f)) * h = F [;] (x,(f * h))