let X be set ; :: thesis: E_Funcs X is Subset of (E_PFuncs X)
E_Funcs X c= E_PFuncs X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in E_Funcs X or x in E_PFuncs X )
assume x in E_Funcs X ; :: thesis: x in E_PFuncs X
then x is Function of X,ExtREAL by Def11;
hence x in E_PFuncs X by Def10; :: thesis: verum

end;

hence E_Funcs X is Subset of (E_PFuncs X) ; :: thesis: verum