theorem :: SETWISEO:23

for X, Y being non empty set
for F being BinOp of Y
for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for B, C being Element of Fin X st B <> {} & B c= C holds
F . ((F $$ (B,f)),(F $$ (C,f))) = F $$ (C,f)