theorem Th17: :: MESFUN9C:17

for X being non empty set
for F being Functional_Sequence of X,REAL st F is with_the_same_dom holds
Partial_Sums F is with_the_same_dom