theorem :: GROUP_4:27

for n being Nat
for G being Group
for I being FinSequence of INT st len I = n holds
(n |-> (1_ G)) |^ I = n |-> (1_ G)