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

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

hence
lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))
by A7, A5, PARTFUN1:5; :: thesis: verum
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;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