theorem :: MESFUN9C:31

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