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, c being Element of X holds F $$ {.a,b,c.},f = F . (F . (f . a),(f . b)),(f . c)
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, c being Element of X holds F $$ {.a,b,c.},f = F . (F . (f . a),(f . b)),(f . c)
let f be Function of X,Y; :: thesis: ( F is idempotent & F is commutative & F is associative implies for a, b, c being Element of X holds F $$ {.a,b,c.},f = F . (F . (f . a),(f . b)),(f . c) )
assume A1: ( F is idempotent & F is commutative & F is associative ) ; :: thesis: for a, b, c being Element of X holds F $$ {.a,b,c.},f = F . (F . (f . a),(f . b)),(f . c)
let a, b, c be Element of X; :: thesis: F $$ {.a,b,c.},f = F . (F . (f . a),(f . b)),(f . c)
consider G being Function of (Fin X),Y such that
A2: F $$ {.a,b,c.},f = G . {a,b,c} 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,c} & B' <> {} holds
for x being Element of X st x in {a,b,c} holds
G . (B' \/ {x}) = F . (G . B'),(f . x) by A1, Th25;
A5: b in {a,b,c} by ENUMSET1:def 1;
A6: G . {a,b} = G . ({a} \/ {b}) by ENUMSET1:41
.= F . (G . {.a.}),(f . b) by A4, A5, Th3
.= F . (f . a),(f . b) by A3 ;
A7: c in {a,b,c} by ENUMSET1:def 1;
thus F $$ {.a,b,c.},f = G . ({.a,b.} \/ {.c.}) by A2, ENUMSET1:43
.= F . (F . (f . a),(f . b)),(f . c) by A4, A6, A7, Th4 ; :: thesis: verum