:: deftheorem Def6 defines power BCIALG_4:def 6 :
for X being BCI-Algebra_with_Condition(S)
for b₂ being Function of [: the carrier of X,NAT:], the carrier of X holds
( b₂ = power X iff for h being Element of X holds
( b₂ . (h,0) = 0. X & ( for n being Nat holds b₂ . (h,(n + 1)) = (b₂ . (h,n)) * h ) ) );