set x = the Functor of C,D;
the Functor of C,D in Funct (C,D) by Def2;
hence not Funct (C,D) is empty ; :: thesis: verum