let X, Y be non empty set ; 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; ( 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
; 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; 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; ( f .: A = g .: B implies F $$ (A,f) = F $$ (B,g) )
assume A4:
f .: A = g .: B
; F $$ (A,f) = F $$ (B,g)
now ( A = {} implies F $$ (A,f) = F $$ (B,g) )assume A5:
A = {}
;
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;
verum end;
hence
F $$ (A,f) = F $$ (B,g)
by A1, A2, A4, Th23; verum