theorem :: FUNCOP_1:50

for X, Y being non empty set
for F being BinOp of X
for f being Function of Y,X
for x being Element of X holds (F [:] ((id X),x)) * f = F [:] (f,x)