for F being FinSequence of ExtREAL st ( for n being Nat st n in dom F holds
0 <= F . n ) holds
0 <= Sum F