let f be Function; :: thesis: ( f is empty-yielding implies f is natural-valued )
assume f is empty-yielding ; :: thesis: f is natural-valued
then ( 0 in NAT & ( for x being object st x in rng f holds
x = 0 ) ) by RELAT_1:149;
then for x being object st x in rng f holds
x in NAT ;
hence f is natural-valued by TARSKI:def 3, VALUED_0:def 6; :: thesis: verum