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