theorem Th24: :: LOPBAN_4:24
for X being Banach_Algebra
for w, z being Element of X
for k being Nat holds (z rExpSeq) . k = (Expan_e (k,z,w)) . k