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 (Partial_Sums F))
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 (Partial_Sums F))
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 (Partial_Sums F)) )
assume that
A1: F is additive and
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 (Partial_Sums F))
set G = - F;
for n being Element of NAT holds (Partial_Sums (- F)) . n = (- (Partial_Sums F)) . n by Th42;
then A4: Partial_Sums (- F) = - (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 (Partial_Sums F))) = dom (lim (Partial_Sums F)) by MESFUNC1:def 7;
then A7: dom (- (lim (Partial_Sums F))) = dom ((Partial_Sums F) . 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 (Partial_Sums F))) . x

proof

let x be Element of X; :: thesis: ( x in dom (lim (Partial_Sums (- F))) implies (lim (Partial_Sums (- F))) . x = (- (lim (Partial_Sums F))) . x )
assume A8: x in dom (lim (Partial_Sums (- F))) ; :: thesis: (lim (Partial_Sums (- F))) . x = (- (lim (Partial_Sums F))) . 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 A1, A2, A8, A5, MESFUNC9:33;
(Partial_Sums (- F)) # x = - ((Partial_Sums F) # x) by A4, Th38;
then A10: lim ((Partial_Sums (- F)) # x) = - (lim ((Partial_Sums F) # x)) by A9, DBLSEQ_3:17;
(- (lim (Partial_Sums F))) . x = - ((lim (Partial_Sums F)) . x) by A7, A5, A8, MESFUNC1:def 7;
then (- (lim (Partial_Sums F))) . x = - (lim ((Partial_Sums F) # x)) by A7, A5, A8, A6, MESFUNC8:def 9;
hence (lim (Partial_Sums (- F))) . x = (- (lim (Partial_Sums F))) . x by A8, A10, MESFUNC8:def 9; :: thesis: verum

end;

hence lim (Partial_Sums (- F)) = - (lim (Partial_Sums F)) by A7, A5, PARTFUN1:5; :: thesis: verum