theorem Th8: :: MESFUN9C:8

for X being non empty set
for F being Functional_Sequence of X,REAL
for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds
( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )