theorem Th25: :: FUNCOP_1:25

for f, g, h, F being Function holds (F .: (f,g)) * h = F .: ((f * h),(g * h))