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