let C, D be non empty set ; :: thesis: for c1, c2, c3 being Element of C
for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 holds
F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
let c1, c2, c3 be Element of C; :: thesis: for F being BinOp of D
for f being Function of C,D st F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 holds
F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
let F be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 holds
F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
let f be Function of C,D; :: thesis: ( F is commutative & F is associative & c1 <> c2 & c1 <> c3 & c2 <> c3 implies F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3)) )
assume that
A1: ( F is commutative & F is associative ) and
A2: c1 <> c2 ; :: thesis: ( not c1 <> c3 or not c2 <> c3 or F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3)) )
assume ( c1 <> c3 & c2 <> c3 ) ; :: thesis: F $$ ({.c1,c2,c3.},f) = F . ((F . ((f . c1),(f . c2))),(f . c3))
then A3: not c3 in {c1,c2} by TARSKI:def 2;
thus F $$ ({.c1,c2,c3.},f) = F $$ (({.c1,c2.} \/ {.c3.}),f) by ENUMSET1:3
.= F . ((F $$ ({.c1,c2.},f)),(f . c3)) by A1, A3, Th4
.= F . ((F . ((f . c1),(f . c2))),(f . c3)) by A1, A2, Th3 ; :: thesis: verum