for X being BCI-algebra
for x being Element of X
for n, m being Nat st ((0. X),x) to_power m = 0. X holds
((0. X),x) to_power (m * n) = 0. X