theorem Th3: :: GROUPP_1:3

for G being Group
for a being Element of G
for n being Nat st a |^ n = 1_ G holds
(a ") |^ n = 1_ G