:: deftheorem Def1 defines to_power BCIALG_2:def 1 :
for X being BCI-algebra
for x, y being Element of X
for n being Nat
for b₅ being Element of X holds
( b₅ = (x,y) to_power n iff ex f being sequence of the carrier of X st
( b₅ = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) ) );