theorem Th11: :: MESFUN9C:11

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