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

C is integer-functions-membered ;

hence I_Funcs X is integer-functions-membered ; :: thesis: verum