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

proof

let x be object ; :: 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 (Q_PFuncs X) ; :: thesis: verum