:: deftheorem Def10 defines exp_ LOPBAN_4:def 10 :
for X being 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 rExpSeq) );