theorem Th9: :: BCIALG_2:9

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