:: deftheorem Def1 defines BCI-power BCIALG_6:def 1 :
for G being non empty BCIStr_0
for b₂ being Function of [: the carrier of G,NAT:], the carrier of G holds
( b₂ = BCI-power G iff for x being Element of G holds
( b₂ . (x,0) = 0. G & ( for n being Nat holds b₂ . (x,(n + 1)) = x \ ((b₂ . (x,n)) `) ) ) );