theorem PosLeq: :: RVSUM_3:10

for f being constant non empty real-valued positive FinSequence holds the_value_of f > 0