take { the natural-valued Function} ; :: thesis: ( { the natural-valued Function} is natural-functions-membered & not { the natural-valued Function} is empty )
thus for x being object st x in { the natural-valued Function} holds
x is natural-valued Function by TARSKI:def 1; :: according to VALUED_2:def 7 :: thesis: not { the natural-valued Function} is empty
thus not { the natural-valued Function} is empty ; :: thesis: verum