theorem Th26: :: SETWISEO:29

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