let f be constant non empty real-valued positive FinSequence; :: thesis: the_value_of f > 0
consider x being set such that
A1: ( x in dom f & the_value_of f = f . x ) by FUNCT_1:def 12;
thus the_value_of f > 0 by A1, PosDef; :: thesis: verum