theorem :: BCIALG_2:14

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