reconsider C = C_Funcs X as Subset of by Th1;
C is complex-functions-membered ;
hence C_Funcs X is complex-functions-membered ; :: thesis: verum