reconsider C = E_Funcs X as Subset of (E_PFuncs X) by Th2;
C is ext-real-functions-membered ;
hence E_Funcs X is ext-real-functions-membered ; :: thesis: verum