let X be set ; :: thesis: N_Funcs X is Subset of (N_PFuncs X)

N_Funcs X c= N_PFuncs X

N_Funcs X c= N_PFuncs X

proof

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

assume x in N_Funcs X ; :: thesis: x in N_PFuncs X

then x is Function of X,NAT by Def19;

hence x in N_PFuncs X by Def18; :: thesis: verum

end;assume x in N_Funcs X ; :: thesis: x in N_PFuncs X

then x is Function of X,NAT by Def19;

hence x in N_PFuncs X by Def18; :: thesis: verum