theorem Th15: :: BCIALG_6:15

for X being BCI-algebra
for a, b being Element of AtomSet X
for n being Nat holds (a \ b) |^ n = (a |^ n) \ (b |^ n)