:: deftheorem Def7 defines power GROUP_1:def 7 :
for G being non empty multMagma
for b₂ being Function of [: the carrier of G,NAT:], the carrier of G holds
( b₂ = power G iff for h being Element of G holds
( b₂ . (h,0) = 1_ G & ( for n being Nat holds b₂ . (h,(n + 1)) = (b₂ . (h,n)) * h ) ) );