for G being Group
for a being Element of G
for I being FinSequence of INT holds Product (((len I) |-> a) |^ I) = a |^ (Sum I)