let C, D be non empty set ; :: thesis: for c1, c2 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 holds

F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))

let c1, c2 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 holds

F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))

let F be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & c1 <> c2 holds

F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))

let f be Function of C,D; :: thesis: ( F is commutative & F is associative & c1 <> c2 implies F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2)) )

assume that

A1: ( F is commutative & F is associative ) and

A2: c1 <> c2 ; :: thesis: F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))

consider g being Function of (Fin C),D such that

A3: F $$ ({.c1,c2.},f) = g . {c1,c2} and

for e being Element of D st e is_a_unity_wrt F holds

g . {} = e and

A4: for c being Element of C holds g . {c} = f . c and

A5: for B being Element of Fin C st B c= {c1,c2} & B <> {} holds

for c being Element of C st c in {c1,c2} \ B holds

g . (B \/ {c}) = F . ((g . B),(f . c)) by A1, SETWISEO:def 3;

( c1 in {c1} & not c2 in {c1} ) by A2, TARSKI:def 1;

then {c1,c2} \ {c1} = {c2} by ZFMISC_1:62;

then A6: c2 in {c1,c2} \ {c1} by TARSKI:def 1;

thus F $$ ({.c1,c2.},f) = g . ({.c1.} \/ {.c2.}) by A3, ENUMSET1:1

.= F . ((g . {c1}),(f . c2)) by A5, A6, ZFMISC_1:7

.= F . ((f . c1),(f . c2)) by A4 ; :: thesis: verum

for F being BinOp of D

for f being Function of C,D st F is commutative & F is associative & c1 <> c2 holds

F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))

let c1, c2 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 holds

F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))

let F be BinOp of D; :: thesis: for f being Function of C,D st F is commutative & F is associative & c1 <> c2 holds

F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))

let f be Function of C,D; :: thesis: ( F is commutative & F is associative & c1 <> c2 implies F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2)) )

assume that

A1: ( F is commutative & F is associative ) and

A2: c1 <> c2 ; :: thesis: F $$ ({.c1,c2.},f) = F . ((f . c1),(f . c2))

consider g being Function of (Fin C),D such that

A3: F $$ ({.c1,c2.},f) = g . {c1,c2} and

for e being Element of D st e is_a_unity_wrt F holds

g . {} = e and

A4: for c being Element of C holds g . {c} = f . c and

A5: for B being Element of Fin C st B c= {c1,c2} & B <> {} holds

for c being Element of C st c in {c1,c2} \ B holds

g . (B \/ {c}) = F . ((g . B),(f . c)) by A1, SETWISEO:def 3;

( c1 in {c1} & not c2 in {c1} ) by A2, TARSKI:def 1;

then {c1,c2} \ {c1} = {c2} by ZFMISC_1:62;

then A6: c2 in {c1,c2} \ {c1} by TARSKI:def 1;

thus F $$ ({.c1,c2.},f) = g . ({.c1.} \/ {.c2.}) by A3, ENUMSET1:1

.= F . ((g . {c1}),(f . c2)) by A5, A6, ZFMISC_1:7

.= F . ((f . c1),(f . c2)) by A4 ; :: thesis: verum