let f, g, F, h be Function; ( 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))
; h = F .: (f,g)
hence
h = F .: (f,g)
by A1; verum