theorem Th14: :: LOPBAN_4:14

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