let C, D be non empty set ; :: thesis: for B being Element of Fin C
for F being BinOp of D
for f, f' being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . (F $$ B,f),(F $$ B,f') = F $$ B,(F .: f,f')
let B be Element of Fin C; :: thesis: for F being BinOp of D
for f, f' being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . (F $$ B,f),(F $$ B,f') = F $$ B,(F .: f,f')
let F be BinOp of D; :: thesis: for f, f' being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . (F $$ B,f),(F $$ B,f') = F $$ B,(F .: f,f')
let f, f' be Function of C,D; :: thesis: ( F is commutative & F is associative & F is having_a_unity implies F . (F $$ B,f),(F $$ B,f') = F $$ B,(F .: f,f') )
set e = the_unity_wrt F;
assume A1: ( F is commutative & F is associative & F is having_a_unity ) ; :: thesis: F . (F $$ B,f),(F $$ B,f') = F $$ B,(F .: f,f')
then ( F . (the_unity_wrt F),(the_unity_wrt F) = the_unity_wrt F & ( for d1, d2, d3, d4 being Element of D holds F . (F . d1,d2),(F . d3,d4) = F . (F . d1,d3),(F . d2,d4) ) ) by Lm3, SETWISEO:23;
hence F . (F $$ B,f),(F $$ B,f') = F $$ B,(F .: f,f') by A1, Th11; :: thesis: verum