theorem Th23: :: BCIALG_6:23

for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) |^ j = a |^ (i * j)