theorem Th4: :: GROUPP_1:4

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