let X be non empty set ; :: thesis: 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 ())

let S be SigmaField of X; :: thesis: 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 ())

let F be Functional_Sequence of X,ExtREAL; :: thesis: ( 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 ) implies lim (Partial_Sums (- F)) = - (lim ()) )

assume that
A2: F is with_the_same_dom and
A3: for x being Element of X st x in dom (F . 0) holds
F # x is summable ; :: thesis: lim (Partial_Sums (- F)) = - (lim ())
set G = - F;
for n being Element of NAT holds (Partial_Sums (- F)) . n = (- ()) . n by Th42;
then A4: Partial_Sums (- F) = - () by FUNCT_2:def 7;
A5: dom (lim (Partial_Sums (- F))) = dom ((Partial_Sums (- F)) . 0) by MESFUNC8:def 9
.= dom ((- F) . 0) by MESFUNC9:def 4
.= dom (- (F . 0)) by Th37
.= dom (F . 0) by MESFUNC1:def 7 ;
A6: dom (- (lim ())) = dom (lim ()) by MESFUNC1:def 7;
then A7: dom (- (lim ())) = dom (() . 0) by MESFUNC8:def 9
.= dom (F . 0) by MESFUNC9:def 4 ;
for x being Element of X st x in dom (lim (Partial_Sums (- F))) holds
(lim (Partial_Sums (- F))) . x = (- (lim ())) . x
proof
let x be Element of X; :: thesis: ( x in dom (lim (Partial_Sums (- F))) implies (lim (Partial_Sums (- F))) . x = (- (lim ())) . x )
assume A8: x in dom (lim (Partial_Sums (- F))) ; :: thesis: (lim (Partial_Sums (- F))) . x = (- (lim ())) . x
then F # x is summable by A3, A5;
then Partial_Sums (F # x) is convergent by MESFUNC9:def 2;
then A9: (Partial_Sums F) # x is convergent by ;
(Partial_Sums (- F)) # x = - (() # x) by ;
then A10: lim ((Partial_Sums (- F)) # x) = - (lim (() # x)) by ;
(- (lim ())) . x = - ((lim ()) . x) by ;
then (- (lim ())) . x = - (lim (() # x)) by ;
hence (lim (Partial_Sums (- F))) . x = (- (lim ())) . x by ; :: thesis: verum
end;
hence lim (Partial_Sums (- F)) = - (lim ()) by ; :: thesis: verum