let X be set ; :: thesis: C_Funcs X is Subset of (C_PFuncs X)

C_Funcs X c= C_PFuncs X

C_Funcs X c= C_PFuncs X

proof

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

assume x in C_Funcs X ; :: thesis: x in C_PFuncs X

then x is Function of X,COMPLEX by Def9;

hence x in C_PFuncs X by Def8; :: thesis: verum

end;assume x in C_Funcs X ; :: thesis: x in C_PFuncs X

then x is Function of X,COMPLEX by Def9;

hence x in C_PFuncs X by Def8; :: thesis: verum