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