for n being Nat
for G being Group
for a being Element of G holds Product (n |-> a) = a |^ n