theorem Th9:
for
C,
D being non
empty set for
B being
Element of
Fin C for
e being
Element of
D 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 &
e = the_unity_wrt F &
G . (
e,
e)
= e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (
(G . (d1,d2)),
(G . (d3,d4)))
= G . (
(F . (d1,d3)),
(F . (d2,d4))) ) holds
G . (
(F $$ (B,f)),
(F $$ (B,f9)))
= F $$ (
B,
(G .: (f,f9)))