theorem :: BCIALG_4:28

for n being Nat
for X being BCI-Algebra_with_Condition(S)
for x, a being Element of X holds (x,a) to_power n = x \ (a |^ n)