:: deftheorem defines |^ FVALUAT1:def 6 :
for G being non empty doubleLoopStr
for g being Element of G
for n being Nat holds g |^ n = (power G) . (g,n);