:: deftheorem Def2 defines pow POLYNOM8:def 3 :
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for a being Element of L
for i being Integer holds
( ( 0 <= i implies pow (a,i) = (power L) . (a,i) ) & ( not 0 <= i implies pow (a,i) = ((power L) . (a,|.i.|)) " ) );