theorem :: FUNCOP_1:85

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