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