theorem Th27: :: POLYNOM8:27

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for x being Element of L
for i, k being Element of NAT st 1 <= k holds
pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1))