let X be set ; :: thesis: Q_Funcs X is Subset of
Q_Funcs X c= Q_PFuncs X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q_Funcs X or x in Q_PFuncs X )
assume x in Q_Funcs X ; :: thesis: x in Q_PFuncs X
then x is Function of X, RAT by Def15;
hence x in Q_PFuncs X by Def14; :: thesis: verum

end;

hence Q_Funcs X is Subset of ; :: thesis: verum