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