theorem Th49: :: MESFUN11:49

for X being non empty set
for S being SigmaField of X
for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom & ( for x being Element of X st x in dom (F . 0) holds
F # x is summable ) holds
lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))