theorem :: SETWISEO:33

for X, Y being non empty set
for F being BinOp of Y
for f being Function of X,Y st F is idempotent & F is commutative & F is associative & F is having_a_unity holds
for B1, B2 being Element of Fin X holds F $$ ((B1 \/ B2),f) = F . ((F $$ (B1,f)),(F $$ (B2,f)))