theorem :: SETWISEO:27

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 . (a,(F $$ (B,f))) = F $$ (B,(G [;] (a,f)))