for G being Group
for H being Subgroup of G
for a being Element of G st a in H holds
for j being Integer holds a |^ j in H