let X be set ; :: thesis: I_Funcs X is Subset of (I_PFuncs X)

I_Funcs X c= I_PFuncs X

I_Funcs X c= I_PFuncs X

proof

hence
I_Funcs X is Subset of (I_PFuncs X)
; :: thesis: verum
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;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