reconsider C = C_Funcs X as Subset of (C_PFuncs X) by Th1;

C is complex-functions-membered ;

hence C_Funcs X is complex-functions-membered ; :: thesis: verum

C is complex-functions-membered ;

hence C_Funcs X is complex-functions-membered ; :: thesis: verum