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

C is rational-functions-membered ;

hence Q_Funcs X is rational-functions-membered ; :: thesis: verum