theorem Th42: :: MESFUN11:42

for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat holds (Partial_Sums (- F)) . n = (- (Partial_Sums F)) . n