for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive holds
( (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} & (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} )