theorem :: FUNCOP_1:42

for X being non empty set
for F being BinOp of X
for x being Element of X
for g being Function of X,X holds (F .: ((id X),g)) . x = F . (x,(g . x))