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