theorem :: LOPBAN_4:34

for X being Banach_Algebra
for z being Element of X holds exp z = Sum (z rExpSeq) by Def10;