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)

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

let 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;

hence h = F .: (f,g) by FUNCT_2:63; :: thesis: verum