theorem :: FUNCOP_1:41

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