theorem Th20: :: LOPBAN_4:20

for X being Banach_Algebra holds
( (0. X) rExpSeq is norm_summable & Sum ((0. X) rExpSeq) = 1. X )