take {} ; :: thesis: {} is natural-functions-valued
thus {} is natural-functions-valued ; :: thesis: verum