let X be non empty set ; 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; 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; 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 ; ( 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
; ex m being Nat st
( m <= n & (F . m) . z = -infty )
now ex m being Nat st
( m <= n & not (F . m) . z <> -infty )defpred S1[
Nat]
means ( $1
<= n implies
((Partial_Sums F) . $1) . z <> -infty );
assume A3:
for
m being
Nat st
m <= n holds
(F . m) . z <> -infty
;
contradictionA4:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
assume A6:
k + 1
<= n
;
((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:17;
verum
end;
(Partial_Sums F) . 0 = F . 0
by Def4;
then A12:
S1[
0 ]
by A3;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A12, A4);
hence
contradiction
by A2;
verum end;
hence
ex m being Nat st
( m <= n & (F . m) . z = -infty )
; verum