let f be INT -valued Function; :: thesis: ( f is nonnegative-yielding implies f is natural-valued )
assume f is nonnegative-yielding ; :: thesis: f is natural-valued
then for i being object holds f . i is natural ;
hence f is natural-valued by VALUED_0:12; :: thesis: verum