theorem :: GROUP_1:48

for i being Integer
for A being commutative Group
for a, b being Element of A holds (a * b) |^ i = (a |^ i) * (b |^ i) by Th37;