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