let f, g, F, h be Function; :: thesis: ( 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) ) implies h = F .: f,g )
assume that
A1: dom h = dom (F .: f,g) and
A2: for z being set st z in dom (F .: f,g) holds
h . z = F . (f . z),(g . z) ; :: thesis: h = F .: f,g

now

let z be set ; :: thesis: ( z in dom (F .: f,g) implies h . z = (F .: f,g) . z )
assume A3: z in dom (F .: f,g) ; :: thesis: h . z = (F .: f,g) . z
hence h . z = F . (f . z),(g . z) by A2
.= (F .: f,g) . z by A3, Lm1 ;
:: thesis: verum

end;

hence h = F .: f,g by A1, FUNCT_1:9; :: thesis: verum