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