reconsider C = I_Funcs X as Subset of (I_PFuncs X) by Th5;
C is integer-functions-membered ;
hence I_Funcs X is integer-functions-membered ; :: thesis: verum