for F being FinSequence of ExtREAL st ( for i being Nat st i in dom F holds
F . i <> -infty ) holds
Sum F <> -infty