:: deftheorem Def8 defines |^ GROUP_1:def 8 :
for G being Group
for h being Element of G
for i being Integer holds
( ( 0 <= i implies h |^ i = (power G) . (h,|.i.|) ) & ( not 0 <= i implies h |^ i = ((power G) . (h,|.i.|)) " ) );