theorem Th22: :: POLYNOM8:22

for L being non empty non degenerated right_complementable almost_left_invertible left-distributive well-unital add-associative right_zeroed associative commutative doubleLoopStr
for k being Element of NAT
for x being Element of L st x <> 0. L holds
pow ((x "),k) = pow (x,(- k))