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:43
.= 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