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

C is natural-functions-membered ;

hence N_Funcs X is natural-functions-membered ; :: thesis: verum