for G being Group
for H being Subgroup of G
for a being Element of H
for b being Element of G st a = b holds
for n being Element of NAT holds a |^ n = b |^ n by GROUP_4:1;