let X be 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}) = {} )
let F be 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 n be Nat; ( 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
; ( (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} & (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} )
now 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}
;
contradictionA4:
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;
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; (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {}
now 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}
;
contradictionA11:
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;
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; verum