for X being non empty set
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)) )