theorem Th8: :: BASEL_2:8

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