let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for n being Nat
for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty holds
ex m being Nat st
( m <= n & (F . m) . z = -infty )
let F be Functional_Sequence of X,ExtREAL ; :: thesis: for n being Nat
for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty holds
ex m being Nat st
( m <= n & (F . m) . z = -infty )
let n be Nat; :: thesis: for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty holds
ex m being Nat st
( m <= n & (F . m) . z = -infty )
let z be set ; :: thesis: ( z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty implies ex m being Nat st
( m <= n & (F . m) . z = -infty ) )
set PF = Partial_Sums F;
assume A2: ( z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty ) ; :: thesis: ex m being Nat st
( m <= n & (F . m) . z = -infty )

now

assume A4: for m being Nat st m <= n holds
(F . m) . z <> -infty ; :: thesis: contradiction
defpred S₁[ Nat] means ( $1 <= n implies ((Partial_Sums F) . $1) . z <> -infty );
(Partial_Sums F) . 0 = F . 0 by Def0;
then A5: S₁[ 0 ] by A4;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
assume B2: k + 1 <= n ; :: thesis: ((Partial_Sums F) . (k + 1)) . z <> -infty
then k <= n by NAT_1:13;
then ( z in dom ((Partial_Sums F) . k) & z in dom (F . (k + 1)) ) by A2, B2, Lem02;
then B3: z in (dom ((Partial_Sums F) . k)) /\ (dom (F . (k + 1))) by XBOOLE_0:def 4;
B4: ( ((Partial_Sums F) . k) . z <> -infty & (F . (k + 1)) . z <> -infty ) by A4, B1, B2, NAT_1:13;
then ( not ((Partial_Sums F) . k) . z in {-infty } & not (F . (k + 1)) . z in {-infty } ) by TARSKI:def 1;
then ( not z in ((Partial_Sums F) . k) " {-infty } & not z in (F . (k + 1)) " {-infty } ) by FUNCT_1:def 13;
then ( not z in (((Partial_Sums F) . k) " {-infty }) /\ ((F . (k + 1)) " {+infty }) & not z in (((Partial_Sums F) . k) " {+infty }) /\ ((F . (k + 1)) " {-infty }) ) by XBOOLE_0:def 4;
then not z in ((((Partial_Sums F) . k) " {-infty }) /\ ((F . (k + 1)) " {+infty })) \/ ((((Partial_Sums F) . k) " {+infty }) /\ ((F . (k + 1)) " {-infty })) by XBOOLE_0:def 3;
then B5: z in ((dom ((Partial_Sums F) . k)) /\ (dom (F . (k + 1)))) \ (((((Partial_Sums F) . k) " {-infty }) /\ ((F . (k + 1)) " {+infty })) \/ ((((Partial_Sums F) . k) " {+infty }) /\ ((F . (k + 1)) " {-infty }))) by B3, XBOOLE_0:def 5;
B6: (Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1)) by Def0;
then z in dom ((Partial_Sums F) . (k + 1)) by B5, MESFUNC1:def 3;
then ((Partial_Sums F) . (k + 1)) . z = (((Partial_Sums F) . k) . z) + ((F . (k + 1)) . z) by B6, MESFUNC1:def 3;
hence ((Partial_Sums F) . (k + 1)) . z <> -infty by B4, SUPINF_2:9; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
hence contradiction by A2; :: thesis: verum

end;

hence ex m being Nat st
( m <= n & (F . m) . z = -infty ) ; :: thesis: verum