theorem :: SETWOP_2:10

for C, D being non empty set
for B being Element of Fin C
for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(F .: (f,f9)))