let X be set ; :: thesis: I_Funcs X is Subset of (I_PFuncs X)
I_Funcs X c= I_PFuncs X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in I_Funcs X or x in I_PFuncs X )
assume x in I_Funcs X ; :: thesis: x in I_PFuncs X
then x is Function of X,INT by Def17;
hence x in I_PFuncs X by Def16; :: thesis: verum
end;
hence I_Funcs X is Subset of (I_PFuncs X) ; :: thesis: verum