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