let g be subsequence of f; :: thesis: g is nonnegative-yielding
let r be Real; :: according to PARTFUN3:def 4 :: thesis: ( not r in rng g or 0 <= r )
rng g c= rng f by VALUED_0:21;
hence ( not r in rng g or 0 <= r ) by PARTFUN3:def 4; :: thesis: verum