( rng (X --> N) c= {N} & {N} c= ExtNAT ) by ThSubset;
hence X --> N is ext-natural-valued ; :: thesis: verum