let X be non empty set ; :: thesis: 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}) = {} )
let F be Functional_Sequence of X,ExtREAL; :: thesis: 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}) = {} )
let n be Nat; :: thesis: ( F is additive implies ( (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} & (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} ) )
set PF = Partial_Sums F;
assume A1: F is additive ; :: thesis: ( (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} & (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} )

now :: thesis: for z being object holds
( not z in ((Partial_Sums F) . n) " {-infty} or not z in (F . (n + 1)) " {+infty} )

given z being object such that A2: z in ((Partial_Sums F) . n) " {-infty} and
A3: z in (F . (n + 1)) " {+infty} ; :: thesis: contradiction
A4: z in dom ((Partial_Sums F) . n) by A2, FUNCT_1:def 7;
((Partial_Sums F) . n) . z in {-infty} by A2, FUNCT_1:def 7;
then ((Partial_Sums F) . n) . z = -infty by TARSKI:def 1;
then consider k being Nat such that
A5: k <= n and
A6: (F . k) . z = -infty by A4, Th25;
A7: z in dom (F . (n + 1)) by A3, FUNCT_1:def 7;
(F . (n + 1)) . z in {+infty} by A3, FUNCT_1:def 7;
then A8: (F . (n + 1)) . z = +infty by TARSKI:def 1;
z in dom (F . k) by A4, A5, Th22;
then z in (dom (F . k)) /\ (dom (F . (n + 1))) by A7, XBOOLE_0:def 4;
hence contradiction by A1, A8, A6; :: thesis: verum

end;

then ((Partial_Sums F) . n) " {-infty} misses (F . (n + 1)) " {+infty} by XBOOLE_0:3;
hence (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} by XBOOLE_0:def 7; :: thesis: (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {}

now :: thesis: for z being object holds
( not z in ((Partial_Sums F) . n) " {+infty} or not z in (F . (n + 1)) " {-infty} )

given z being object such that A9: z in ((Partial_Sums F) . n) " {+infty} and
A10: z in (F . (n + 1)) " {-infty} ; :: thesis: contradiction
A11: z in dom ((Partial_Sums F) . n) by A9, FUNCT_1:def 7;
((Partial_Sums F) . n) . z in {+infty} by A9, FUNCT_1:def 7;
then ((Partial_Sums F) . n) . z = +infty by TARSKI:def 1;
then consider k being Nat such that
A12: k <= n and
A13: (F . k) . z = +infty by A11, Th23;
A14: z in dom (F . (n + 1)) by A10, FUNCT_1:def 7;
(F . (n + 1)) . z in {-infty} by A10, FUNCT_1:def 7;
then A15: (F . (n + 1)) . z = -infty by TARSKI:def 1;
z in dom (F . k) by A11, A12, Th22;
then z in (dom (F . k)) /\ (dom (F . (n + 1))) by A14, XBOOLE_0:def 4;
hence contradiction by A1, A15, A13; :: thesis: verum

end;

then ((Partial_Sums F) . n) " {+infty} misses (F . (n + 1)) " {-infty} by XBOOLE_0:3;
hence (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} by XBOOLE_0:def 7; :: thesis: verum