for X being BCI-algebra
for x, y being Element of X
for n, m being Nat holds (((x,y) to_power n),y) to_power m = (x,y) to_power (n + m)