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 F is idempotent & F is commutative & F is associative & B <> {} holds
for x being Element of X holds F $$ ((B \/ {.x.}),f) = F . ((F $$ (B,f)),(f . x))