theorem Th46: :: MESFUN11:46
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V121() ) holds
F is additive