theorem Th13: :: CLOPBAN4:13

for X being Complex_Banach_Algebra
for z being Element of X
for n being Nat holds
( (z ExpSeq) . (n + 1) = ((1r / (n + 1)) * z) * ((z ExpSeq) . n) & (z ExpSeq) . 0 = 1. X & ||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n )