theorem :: GROUP_3:51

for G being Group
for a being Element of G
for A, B being Subset of G holds (A * B) |^ a c= (A |^ a) * (B |^ a) by Th34;