for R being non empty add-cancelable right_zeroed well-unital distributive associative left_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R
for a being Element of I
for n being Element of NAT st n <> 0 holds
a |^ n in I