theorem :: BCIALG_2:15

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