for x being object st x in NAT * holds
x is natural-valued Function ;
hence NAT * is natural-functions-membered by VALUED_2:def 7; :: thesis: verum