let f be real-valued Function; :: thesis: ( f is empty-yielding implies f is nonnegative-yielding )
assume f is empty-yielding ; :: thesis: f is nonnegative-yielding
then for r being Real st r in rng f holds
r >= 0 ;
hence f is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum