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