let Y, X 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

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 Th48 ; :: thesis: verum

end;

hence h = F .: f,g by FUNCT_2:113; :: thesis: verum