theorem Th29: :: MESFUNC9:29

for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive & F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)