theorem :: SETWOP_2:3

for C, D being non empty set
for c1, c2, c3 being Element of C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 holds
F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))