let X, Y be non empty set ; :: thesis: for F being BinOp of X

for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds

h = F .: (f,g)

let F be BinOp of X; :: thesis: for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds

h = F .: (f,g)

let f, g, h be Function of Y,X; :: thesis: ( ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) implies h = F .: (f,g) )

assume A1: for z being Element of Y holds h . z = F . ((f . z),(g . z)) ; :: thesis: h = F .: (f,g)

for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds

h = F .: (f,g)

let F be BinOp of X; :: thesis: for f, g, h being Function of Y,X st ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) holds

h = F .: (f,g)

let f, g, h be Function of Y,X; :: thesis: ( ( for z being Element of Y holds h . z = F . ((f . z),(g . z)) ) implies h = F .: (f,g) )

assume A1: for z being Element of Y holds h . z = F . ((f . z),(g . z)) ; :: thesis: h = F .: (f,g)

now :: thesis: for z being Element of Y holds h . z = (F .: (f,g)) . z

hence
h = F .: (f,g)
by FUNCT_2:63; :: thesis: verumlet z be Element of Y; :: thesis: h . z = (F .: (f,g)) . z

thus h . z = F . ((f . z),(g . z)) by A1

.= (F .: (f,g)) . z by Th37 ; :: thesis: verum

end;thus h . z = F . ((f . z),(g . z)) by A1

.= (F .: (f,g)) . z by Th37 ; :: thesis: verum