reconsider C = Q_Funcs X as Subset of (Q_PFuncs X) by Th4;
C is rational-functions-membered ;
hence Q_Funcs X is rational-functions-membered ; :: thesis: verum