theorem :: SETWISEO:28

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