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)

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 :: thesis: for z being object st z in dom (F .: (f,g)) holds

h . z = (F .: (f,g)) . z

hence
h = F .: (f,g)
by A1; :: thesis: verumh . z = (F .: (f,g)) . z

let z be object ; :: 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;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