let f, g, h, F be Function; :: thesis: (F .: f,g) * h = F .: (f * h),(g * h)
thus (F .: f,g) * h = F * (<:f,g:> * h) by RELAT_1:55
.= F .: (f * h),(g * h) by FUNCT_3:75 ; :: thesis: verum