theorem Th23: :: GROUP_3:23

for G being Group
for a, b, g being Element of G holds (a * b) |^ g = (a |^ g) * (b |^ g)