theorem Th28: :: MESFUNC9:28

for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive holds
dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }