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 }) = {} ) )
assume A1: F is additive ; :: thesis: ( (((Partial_Sums F) . n) " {-infty }) /\ ((F . (n + 1)) " {+infty }) = {} & (((Partial_Sums F) . n) " {+infty }) /\ ((F . (n + 1)) " {-infty }) = {} )
set PF = Partial_Sums F;

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
Z1: ( z in ((Partial_Sums F) . n) " {-infty } & z in (F . (n + 1)) " {+infty } ) ;
Z2: ( z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z in {-infty } & z in dom (F . (n + 1)) & (F . (n + 1)) . z in {+infty } ) by Z1, FUNCT_1:def 13;
then Z6: ( ((Partial_Sums F) . n) . z = -infty & (F . (n + 1)) . z = +infty ) by TARSKI:def 1;
then consider k being Nat such that
Z3: ( k <= n & (F . k) . z = -infty ) by Z2, Lem05;
z in dom (F . k) by Z2, Z3, Lem02;
then z in (dom (F . k)) /\ (dom (F . (n + 1))) by Z2, XBOOLE_0:def 4;
hence contradiction by A1, Def1a, Z3, Z6; :: 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
Z1: ( z in ((Partial_Sums F) . n) " {+infty } & z in (F . (n + 1)) " {-infty } ) ;
Z2: ( z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z in {+infty } & z in dom (F . (n + 1)) & (F . (n + 1)) . z in {-infty } ) by Z1, FUNCT_1:def 13;
then Z6: ( ((Partial_Sums F) . n) . z = +infty & (F . (n + 1)) . z = -infty ) by TARSKI:def 1;
then consider k being Nat such that
Z3: ( k <= n & (F . k) . z = +infty ) by Z2, Lem03;
z in dom (F . k) by Z2, Z3, Lem02;
then z in (dom (F . k)) /\ (dom (F . (n + 1))) by Z2, XBOOLE_0:def 4;
hence contradiction by A1, Def1a, Z3, Z6; :: 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