for G being Group
for a being Element of G
for F being FinSequence of the carrier of G holds Product (F |^ a) = (Product F) |^ a