theorem :: BCIALG_2:18

for X being BCI-algebra
for x, y being Element of X
for n being Nat holds ((0. X),(x \ y)) to_power n = (((0. X),x) to_power n) \ (((0. X),y) to_power n)