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