theorem Th1: :: GROUP_4:1

for n being Nat
for G being Group
for a being Element of G
for H being Subgroup of G
for h being Element of H st a = h holds
a |^ n = h |^ n