reconsider C = R_Funcs X as Subset of (R_PFuncs X) by Th3;
C is real-functions-membered ;
hence R_Funcs X is real-functions-membered ; :: thesis: verum