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

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, Th40;
B = {}. X by A4, A5, Th19, RELAT_1:149;
hence F $$ A,f = F $$ B,g by A1, A3, A6, Th40; :: thesis: verum

end;

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