theorem LM080: :: PRSUBSET:4

for x being real-valued FinSequence st x <> {} & x is positive holds
0 < Sum x