for X being Complex_Banach_Algebra
for z being Element of X
for k being Nat holds
( ||.((Partial_Sums (z ExpSeq)) . k).|| <= (Partial_Sums (||.z.|| rExpSeq)) . k & (Partial_Sums (||.z.|| rExpSeq)) . k <= Sum (||.z.|| rExpSeq) & ||.((Partial_Sums (z ExpSeq)) . k).|| <= Sum (||.z.|| rExpSeq) )