theorem Th24: :: BCIALG_6:24

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