theorem Th20: :: CLOPBAN4:20

for X being Complex_Banach_Algebra
for w, z being Element of X holds
( (z ExpSeq) . 0 = 1. X & (Expan (0,z,w)) . 0 = 1. X )