theorem Th21: :: SETWISEO:24

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