let X, Y be non empty set ; :: thesis: for F being BinOp of Y
for B being Element of Fin X
for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for a being Element of Y st f .: B = {a} holds
F $$ (B,f) = a
let F be BinOp of Y; :: thesis: for B being Element of Fin X
for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for a being Element of Y st f .: B = {a} holds
F $$ (B,f) = a
let B be Element of Fin X; :: thesis: for f being Function of X,Y st F is commutative & F is associative & F is idempotent holds
for a being Element of Y st f .: B = {a} holds
F $$ (B,f) = a
let f be Function of X,Y; :: thesis: ( F is commutative & F is associative & F is idempotent implies for a being Element of Y st f .: B = {a} holds
F $$ (B,f) = a )
assume A1: ( F is commutative & F is associative & F is idempotent ) ; :: thesis: for a being Element of Y st f .: B = {a} holds
F $$ (B,f) = a
let a be Element of Y; :: thesis: ( f .: B = {a} implies F $$ (B,f) = a )
assume A2: f .: B = {a} ; :: thesis: F $$ (B,f) = a
A3: for b being Element of X st b in B holds
f . b = a

proof

let b be Element of X; :: thesis: ( b in B implies f . b = a )
assume b in B ; :: thesis: f . b = a
then f . b in {a} by A2, FUNCT_2:35;
hence f . b = a by TARSKI:def 1; :: thesis: verum

end;

B <> {} by A2;
hence F $$ (B,f) = a by A1, A3, Th21; :: thesis: verum