let X, Y 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 B9 being Element of Fin X st B9 c= {a,b,c} & B9 <> {} holds
for x being Element of X st x in {a,b,c} holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) by A1, Th13;
A5: b in {a,b,c} by ENUMSET1:def 1;
A6: G . {a,b} = G . ({a} \/ {b}) by ENUMSET1:1
.= F . ((G . {.a.}),(f . b)) by A4, A5, Th1
.= 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:3
.= F . ((F . ((f . a),(f . b))),(f . c)) by A4, A6, A7, Th2 ; :: thesis: verum