let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL

for x being Element of X st F # x is summable holds

( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )

let F be Functional_Sequence of X,ExtREAL; :: thesis: for x being Element of X st F # x is summable holds

( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )

let x be Element of X; :: thesis: ( F # x is summable implies ( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) ) )

assume A1: F # x is summable ; :: thesis: ( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )

then - (F # x) is summable by Th45;

hence (- F) # x is summable by Th38; :: thesis: Sum ((- F) # x) = - (Sum (F # x))

A2: - (F # x) = (- F) # x by Th38;

Partial_Sums (F # x) is convergent by A1, MESFUNC9:def 2;

then lim (- (Partial_Sums (F # x))) = - (lim (Partial_Sums (F # x))) by DBLSEQ_3:17;

then lim (Partial_Sums (- (F # x))) = - (lim (Partial_Sums (F # x))) by Th44;

then lim (Partial_Sums ((- F) # x)) = - (Sum (F # x)) by A2, MESFUNC9:def 3;

hence Sum ((- F) # x) = - (Sum (F # x)) by MESFUNC9:def 3; :: thesis: verum

for x being Element of X st F # x is summable holds

( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )

let F be Functional_Sequence of X,ExtREAL; :: thesis: for x being Element of X st F # x is summable holds

( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )

let x be Element of X; :: thesis: ( F # x is summable implies ( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) ) )

assume A1: F # x is summable ; :: thesis: ( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )

then - (F # x) is summable by Th45;

hence (- F) # x is summable by Th38; :: thesis: Sum ((- F) # x) = - (Sum (F # x))

A2: - (F # x) = (- F) # x by Th38;

Partial_Sums (F # x) is convergent by A1, MESFUNC9:def 2;

then lim (- (Partial_Sums (F # x))) = - (lim (Partial_Sums (F # x))) by DBLSEQ_3:17;

then lim (Partial_Sums (- (F # x))) = - (lim (Partial_Sums (F # x))) by Th44;

then lim (Partial_Sums ((- F) # x)) = - (Sum (F # x)) by A2, MESFUNC9:def 3;

hence Sum ((- F) # x) = - (Sum (F # x)) by MESFUNC9:def 3; :: thesis: verum