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

C is ext-real-functions-membered ;

hence E_Funcs X is ext-real-functions-membered ; :: thesis: verum