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