let X, Y be non empty set ; :: thesis: for F being BinOp of Y st F is commutative & F is associative & F is idempotent & F is having_a_unity holds
for f, g being Function of X,Y
for A, B being Element of Fin X st f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
let F be BinOp of Y; :: thesis: ( F is commutative & F is associative & F is idempotent & F is having_a_unity implies for f, g being Function of X,Y
for A, B being Element of Fin X st f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g) )
assume that
A1: ( F is commutative & F is associative ) and
A2: F is idempotent and
A3: F is having_a_unity ; :: thesis: for f, g being Function of X,Y
for A, B being Element of Fin X st f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
let f, g be Function of X,Y; :: thesis: for A, B being Element of Fin X st f .: A = g .: B holds
F $$ (A,f) = F $$ (B,g)
let A, B be Element of Fin X; :: thesis: ( f .: A = g .: B implies F $$ (A,f) = F $$ (B,g) )
assume A4: f .: A = g .: B ; :: thesis: F $$ (A,f) = F $$ (B,g)

now :: thesis: ( A = {} implies F $$ (A,f) = F $$ (B,g) )

assume A5: A = {} ; :: thesis: F $$ (A,f) = F $$ (B,g)
then A = {}. X ;
then A6: F $$ (A,f) = the_unity_wrt F by A1, A3, Th28;
f .: A = {} by A5;
then B = {}. X by A4, Th10;
hence F $$ (A,f) = F $$ (B,g) by A1, A3, A6, Th28; :: thesis: verum

end;

hence F $$ (A,f) = F $$ (B,g) by A1, A2, A4, Th23; :: thesis: verum