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

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