theorem Th85: :: RVSUM_1:85

for F being real-valued FinSequence st ( for i being Nat st i in dom F holds
0 <= F . i ) & ex i being Nat st
( i in dom F & 0 < F . i ) holds
0 < Sum F