theorem :: BCIALG_2:11

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