theorem :: FUNCT_3:55

for f, g, h being Function holds <:(f * h),(g * h):> = <:f,g:> * h