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 & F is idempotent ) and
A2: 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 A3: f .: A = g .: B ; :: thesis: F $$ A,f = F $$ B,g

now

assume A = {} ; :: thesis: F $$ A,f = F $$ B,g
then ( A = {}. X & B = {}. X ) by A3, Th19, RELAT_1:149;
then ( F $$ A,f = the_unity_wrt F & F $$ B,g = the_unity_wrt F ) by A1, A2, Th40;
hence F $$ A,f = F $$ B,g ; :: thesis: verum

end;

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