for C, D being non empty set
for B being Element of Fin C
for F, G being BinOp of D
for f, f9 being Function of C,D st F is commutative & F is associative & F is having_a_unity & F is having_an_inverseOp & G = F * ((id D),(the_inverseOp_wrt F)) holds
G . ((F $$ (B,f)),(F $$ (B,f9))) = F $$ (B,(G .: (f,f9)))