:: deftheorem Def2 defines |^ BCIALG_6:def 2 :
for X being BCI-algebra
for x being Element of X
for i being Integer holds
( ( 0 <= i implies x |^ i = (BCI-power X) . (x,|.i.|) ) & ( not 0 <= i implies x |^ i = (BCI-power X) . ((x `),|.i.|) ) );