theorem Th19: :: CLOPBAN4:19

for X being Complex_Banach_Algebra holds
( (0. X) ExpSeq is norm_summable & Sum ((0. X) ExpSeq) = 1. X )