:: deftheorem Def6 defines exp_ CLOPBAN4:def 6 :
for X being Complex_Banach_Algebra
for b₂ being Function of the carrier of X, the carrier of X holds
( b₂ = exp_ X iff for z being Element of X holds b₂ . z = Sum (z ExpSeq) );