theorem Th84: :: RVSUM_1:84

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