let Y, X be non empty set ; :: thesis: for F being BinOp of Y
for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds
for a, b being Element of X holds F $$ {.a,b.},f = F . (f . a),(f . b)
let F be BinOp of Y; :: thesis: for f being Function of X,Y st F is idempotent & F is commutative & F is associative holds
for a, b being Element of X holds F $$ {.a,b.},f = F . (f . a),(f . b)
let f be Function of X,Y; :: thesis: ( F is idempotent & F is commutative & F is associative implies for a, b being Element of X holds F $$ {.a,b.},f = F . (f . a),(f . b) )
assume A1: ( F is idempotent & F is commutative & F is associative ) ; :: thesis: for a, b being Element of X holds F $$ {.a,b.},f = F . (f . a),(f . b)
let a, b be Element of X; :: thesis: F $$ {.a,b.},f = F . (f . a),(f . b)
consider G being Function of (Fin X),Y such that
A2: F $$ {.a,b.},f = G . {a,b} and
for e being Element of Y st e is_a_unity_wrt F holds
G . {} = e and
A3: for x being Element of X holds G . {x} = f . x and
A4: for B' being Element of Fin X st B' c= {a,b} & B' <> {} holds
for x being Element of X st x in {a,b} holds
G . (B' \/ {x}) = F . (G . B'),(f . x) by A1, Th25;
A5: b in {a,b} by TARSKI:def 2;
thus F $$ {.a,b.},f = G . ({.a.} \/ {.b.}) by A2, ENUMSET1:41
.= F . (G . {.a.}),(f . b) by A4, A5, ZFMISC_1:12
.= F . (f . a),(f . b) by A3 ; :: thesis: verum