for X being Banach_Algebra
for m being Nat
for seq1, seq2 being sequence of X st ( for n being Nat st n <= m holds
seq1 . n = seq2 . n ) holds
(Partial_Sums seq1) . m = (Partial_Sums seq2) . m