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