theorem Th33:
for
D being non
empty set for
e being
Element of
D for
F,
G being
BinOp of
D for
i being
Nat for
T1,
T2 being
Element of
i -tuples_on 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 "**" T1),
(F "**" T2))
= F "**" (G .: (T1,T2))