reconsider C = N_Funcs X as Subset of by Th6;
C is natural-functions-membered ;
hence N_Funcs X is natural-functions-membered ; :: thesis: verum