theorem Th36: :: POLYNOM5:36

for L being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for x being Element of L
for n being Nat holds <%x%> `^ n = <%(power (x,n))%>