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