theorem :: BCIALG_4:21

for n being Nat
for X being BCI-Algebra_with_Condition(S)
for x being Element of X holds x |^ (n + 1) = (x |^ n) * x by Def6;