theorem Th7: :: MESFUN9C:7

for X being non empty set
for F being Functional_Sequence of X,REAL holds Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)