theorem
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)))