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 that
A1: z in dom ((Partial_Sums F) . n) and
A2: ((Partial_Sums F) . n) . z = +infty ; :: thesis: ex m being Nat st
( m <= n & (F . m) . z = +infty )

now :: thesis: ex m being Element of NAT st
( m <= n & not (F . m) . z <> +infty )

defpred S₁[ Nat] means ( $1 <= n implies ((Partial_Sums F) . $1) . z <> +infty );
assume A3: for m being Element of NAT st m <= n holds
(F . m) . z <> +infty ; :: thesis: contradiction
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
assume A6: k + 1 <= n ; :: thesis: ((Partial_Sums F) . (k + 1)) . z <> +infty
then k <= n by NAT_1:13;
then A7: z in dom ((Partial_Sums F) . k) by A1, Th22;
not ((Partial_Sums F) . k) . z in {+infty} by A5, A6, NAT_1:13, TARSKI:def 1;
then not z in ((Partial_Sums F) . k) " {+infty} by FUNCT_1:def 7;
then A8: not z in (((Partial_Sums F) . k) " {+infty}) /\ ((F . (k + 1)) " {-infty}) by XBOOLE_0:def 4;
z in dom (F . (k + 1)) by A1, A6, Th22;
then A9: z in (dom ((Partial_Sums F) . k)) /\ (dom (F . (k + 1))) by A7, XBOOLE_0:def 4;
A10: (Partial_Sums F) . (k + 1) = ((Partial_Sums F) . k) + (F . (k + 1)) by Def4;
A11: (F . (k + 1)) . z <> +infty by A3, A6;
then not (F . (k + 1)) . z in {+infty} by TARSKI:def 1;
then not z in (F . (k + 1)) " {+infty} by FUNCT_1:def 7;
then 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 A8, XBOOLE_0:def 3;
then 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 A9, XBOOLE_0:def 5;
then z in dom ((Partial_Sums F) . (k + 1)) by A10, MESFUNC1:def 3;
then ((Partial_Sums F) . (k + 1)) . z = (((Partial_Sums F) . k) . z) + ((F . (k + 1)) . z) by A10, MESFUNC1:def 3;
hence ((Partial_Sums F) . (k + 1)) . z <> +infty by A5, A6, A11, NAT_1:13, XXREAL_3:16; :: thesis: verum

end;

(Partial_Sums F) . 0 = F . 0 by Def4;
then A12: S₁[ 0 ] by A3;
for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A4);
hence contradiction by A2; :: thesis: verum

end;

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