let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty & m <= n holds
(F . m) . z <> -infty
let F be Functional_Sequence of X,ExtREAL ; :: thesis: for n, m being Nat
for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty & m <= n holds
(F . m) . z <> -infty
let n, m be Nat; :: thesis: for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty & m <= n holds
(F . m) . z <> -infty
let z be set ; :: thesis: ( F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty & m <= n implies (F . m) . z <> -infty )
assume that
A1: F is additive and
A2: ( z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty ) and
A3: m <= n ; :: thesis: (F . m) . z <> -infty
consider k being Nat such that
A4: ( k <= n & (F . k) . z = +infty ) by A2, Lem03;
( z in dom (F . k) & z in dom (F . m) ) by A2, A3, A4, Lem02;
then z in (dom (F . m)) /\ (dom (F . k)) by XBOOLE_0:def 4;
hence (F . m) . z <> -infty by A4, A1, Def1a; :: thesis: verum