theorem Th18: :: BCIALG_6:18

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