:: deftheorem Def25 defines natural-functions-valued VALUED_2:def 25 :
for R being Relation holds
( R is natural-functions-valued iff rng R is natural-functions-membered );