theorem :: FUNCOP_1:43

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 .: (g,(id X))) . x = F . ((g . x),x)