theorem Th23: :: MESFUNC9:23

for X being 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 )