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