for X being Complex_Banach_Algebra
for z being Element of X
for m, n being Nat holds
( |.((Partial_Sums (||.z.|| rExpSeq)) . n).| = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies |.(((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)).| = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) )