theorem :: FUNCOP_1:62

for X being non empty set
for Y being set
for F being BinOp of X
for f being Function of Y,X
for x1, x2 being Element of X st F is associative holds
F [;] ((F . (x1,x2)),f) = F [;] (x1,(F [;] (x2,f)))