:: deftheorem PosDef defines positive RVSUM_3:def 1 :
for f being real-valued FinSequence holds
( f is positive iff for n being Nat st n in dom f holds
f . n > 0 );