theorem Th47: :: MESFUN11:47

for X being non empty set
for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V120() ) holds
F is additive