take the natural-valued Function ; :: thesis: the natural-valued Function is ext-natural-valued
thus the natural-valued Function is ext-natural-valued ; :: thesis: verum