for X, Y being non empty set
for F being BinOp of X
for f, g being Function of Y,X
for x being Element of X st ( for y being Element of Y holds g . y = F . (x,(f . y)) ) holds
g = F [;] (x,f)