theorem :: GROUP_4:11

for G being Group
for a, b, c being Element of G holds
( Product <*a,b,c*> = (a * b) * c & Product <*a,b,c*> = a * (b * c) )