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

C is real-functions-membered ;

hence R_Funcs X is real-functions-membered ; :: thesis: verum