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

assume ex x being set st
( x in ((Partial_Sums F) . n) " {-infty } & x in (F . (n + 1)) " {+infty } ) ; :: thesis: contradiction
then consider z being set such that
A2: z in ((Partial_Sums F) . n) " {-infty } and
A3: z in (F . (n + 1)) " {+infty } ;
A4: z in dom ((Partial_Sums F) . n) by A2, FUNCT_1:def 13;
((Partial_Sums F) . n) . z in {-infty } by A2, FUNCT_1:def 13;
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 13;
(F . (n + 1)) . z in {+infty } by A3, FUNCT_1:def 13;
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, Def5; :: 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

assume ex x being set st
( x in ((Partial_Sums F) . n) " {+infty } & x in (F . (n + 1)) " {-infty } ) ; :: thesis: contradiction
then consider z being set such that
A9: z in ((Partial_Sums F) . n) " {+infty } and
A10: z in (F . (n + 1)) " {-infty } ;
A11: z in dom ((Partial_Sums F) . n) by A9, FUNCT_1:def 13;
((Partial_Sums F) . n) . z in {+infty } by A9, FUNCT_1:def 13;
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 13;
(F . (n + 1)) . z in {-infty } by A10, FUNCT_1:def 13;
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, Def5; :: 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