let C, D be non empty set ; :: thesis: for B being Element of Fin C
for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . ((F \$\$ (B,f)),(F \$\$ (B,f9))) = F \$\$ (B,(F .: (f,f9)))

let B be Element of Fin C; :: thesis: for F being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . ((F \$\$ (B,f)),(F \$\$ (B,f9))) = F \$\$ (B,(F .: (f,f9)))

let F be BinOp of D; :: thesis: for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity holds
F . ((F \$\$ (B,f)),(F \$\$ (B,f9))) = F \$\$ (B,(F .: (f,f9)))

let f, f9 be Function of C,D; :: thesis: ( F is commutative & F is associative & F is having_a_unity implies F . ((F \$\$ (B,f)),(F \$\$ (B,f9))) = F \$\$ (B,(F .: (f,f9))) )
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,f9))) = F \$\$ (B,(F .: (f,f9)))
then ( 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 ;
hence F . ((F \$\$ (B,f)),(F \$\$ (B,f9))) = F \$\$ (B,(F .: (f,f9))) by ; :: thesis: verum