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, Th2

.= F . ((F . ((f . c1),(f . c2))),(f . c3)) by A1, A2, Th1 ; :: thesis: verum

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, Th2

.= F . ((F . ((f . c1),(f . c2))),(f . c3)) by A1, A2, Th1 ; :: thesis: verum