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