theorem :: FUNCOP_1:39

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