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) and
A3: ((Partial_Sums F) . n) . z = +infty and
A4: m <= n ; :: thesis: (F . m) . z <> -infty
A5: z in dom (F . m) by A2, A4, Th22;
consider k being Nat such that
A6: k <= n and
A7: (F . k) . z = +infty by A2, A3, Th23;
z in dom (F . k) by A2, A6, Th22;
then z in (dom (F . m)) /\ (dom (F . k)) by A5, XBOOLE_0:def 4;
hence (F . m) . z <> -infty by A1, A7; :: thesis: verum