let F be FinSequence; :: thesis: ( F is empty implies F is nonnegative-yielding )
assume F is empty ; :: 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