let f be non empty real-valued Function; :: thesis: ( f is empty-yielding implies not f is negative-yielding )
assume A1: f is empty-yielding ; :: thesis: not f is negative-yielding
take the Element of rng f ; :: according to PARTFUN3:def 2 :: thesis: ( the Element of rng f in rng f & 0 <= the Element of rng f )
thus ( the Element of rng f in rng f & 0 <= the Element of rng f ) by A1; :: thesis: verum