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:36
.= F .: ((f * h),(g * h)) by FUNCT_3:55 ; :: thesis: verum