theorem Th24: :: POLYNOM8:24

for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for x being Element of L
for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m)