:: deftheorem defines |^ GROUP_1:def 9 :
for G being Group
for h being Element of G
for n being natural Number holds h |^ n = (power G) . (h,n);