theorem Th30: :: MESFUNC9:30

for X being non empty set
for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is nonnegative ) holds
F is additive by SUPINF_2:51;