theorem Th10: :: MESFUN9C:10

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