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 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 B9 being Element of Fin X st B9 c= {a,b} & B9 <> {} holds
for x being Element of X st x in {a,b} holds
G . (B9 \/ {x}) = F . ((G . B9),(f . x)) by A1, Th13;
A5: b in {a,b} by TARSKI:def 2;
thus F $$ ({.a,b.},f) = G . ({.a.} \/ {.b.}) by A2, ENUMSET1:1
.= F . ((G . {.a.}),(f . b)) by A4, A5, ZFMISC_1:7
.= F . ((f . a),(f . b)) by A3 ; :: thesis: verum