theorem Th12: :: BCIALG_2:12

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