x .--> N = {x} --> N by FUNCOP_1:def 9;
hence x .--> N is ext-natural-valued ; :: thesis: verum