:: deftheorem defines |^ BCIALG_4:def 7 :
for X being BCI-Algebra_with_Condition(S)
for x being Element of X
for n being Nat holds x |^ n = (power X) . (x,n);