theorem :: FUNCOP_1:40

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