let X be set ; :: thesis: R_Funcs X is Subset of (R_PFuncs X)

R_Funcs X c= R_PFuncs X

R_Funcs X c= R_PFuncs X

proof

hence
R_Funcs X is Subset of (R_PFuncs X)
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R_Funcs X or x in R_PFuncs X )

assume x in R_Funcs X ; :: thesis: x in R_PFuncs X

then x is Function of X,REAL by Def13;

hence x in R_PFuncs X by Def12; :: thesis: verum

end;assume x in R_Funcs X ; :: thesis: x in R_PFuncs X

then x is Function of X,REAL by Def13;

hence x in R_PFuncs X by Def12; :: thesis: verum