theorem Th27: :: LOPBAN_4:27

for X being Banach_Algebra
for z being Element of X
for n being Nat holds 0 <= (||.z.|| rExpSeq) . n