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
then A3: B <> {} by RELAT_1:149;
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:43;
hence f . b = a by TARSKI:def 1; :: thesis: verum

end;

hence F $$ B,f = a by A1, A3, Th33; :: thesis: verum