for m, n being Nat
for X being BCK-algebra
for x, y being Element of X st m > n & (x,y) to_power n = (x,y) to_power m holds
for k being Nat st k >= n holds
(x,y) to_power n = (x,y) to_power k