theorem Th16: :: CLOPBAN3:16

for X being ComplexNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)