theorem Th9: :: MESFUN9C:9

for X being non empty set
for F being Functional_Sequence of X,REAL holds R_EAL F is additive