theorem Th21: :: BCIALG_6:21

for X being BCI-algebra
for x being Element of X
for n being Nat holds (x |^ n) ` = (((x `) `) |^ n) `