theorem :: FUNCOP_1:21

for f, g, F, h being Function st dom h = dom (F .: (f,g)) & ( for z being set st z in dom (F .: (f,g)) holds
h . z = F . ((f . z),(g . z)) ) holds
h = F .: (f,g)