:: deftheorem Def5 defines |^ FVALUAT1:def 5 :
for G being non empty doubleLoopStr
for g being Element of G
for i being Integer holds
( ( 0 <= i implies g |^ i = (power G) . (g,|.i.|) ) & ( not 0 <= i implies g |^ i = / ((power G) . (g,|.i.|)) ) );