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